English
Let κ be a type and R an Additive Monoid with a relation r making sense of boundedness. If hr ensures that the sum of two r-bounded functions is r-bounded and hr0 holds for 0, then for any finite s and any family {u_k} with each u_k r-bounded, the function summing u_k over k ∈ s is r-bounded.
Русский
Пусть κ — тип, R — аддитивный моноид, r — отношение, определяющее ограниченность. Пусть hr защищает от суммирования двумя функциями, ограниченными по r, и hr0 верно для 0. Тогда для любого конечного множества s и семейства {u_k} такая сумма по k ∈ s также ограничена по r.
LaTeX
$$$ r(0,0) \land \Big( \forall k \in s,\ f.IsBoundedUnder\ r\ (u_k) \Big) \Rightarrow f.IsBoundedUnder\ r\left( \sum_{k \in s} u_k \right) $$$
Lean4
theorem isBoundedUnder_sum {κ : Type*} [AddCommMonoid R] {r : R → R → Prop}
(hr : ∀ (v₁ v₂ : α → R), f.IsBoundedUnder r v₁ → f.IsBoundedUnder r v₂ → f.IsBoundedUnder r (v₁ + v₂)) (hr₀ : r 0 0)
{u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, f.IsBoundedUnder r (u k)) : f.IsBoundedUnder r (∑ k ∈ s, u k) :=
by
induction s using Finset.cons_induction
case empty =>
rw [Finset.sum_empty]
exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩
case cons k₀ s k₀_notin_s ih =>
simp only [Finset.forall_mem_cons] at *
simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)
