memLp_finset_sum — Mathlib

English

Let s be a finite set of indices and each f_i be MemLp. Then the sum ∑_{i∈s} f_i is MemLp with exponent p.

Русский

Пусть s — конечное множество индексов, и каждый f_i принадлежит MemLp. Тогда сумма ∑_{i∈s} f_i принадлежит MemLp с экспонентой p.

LaTeX

$$∀ i ∈ s, MemLp (f i) p μ → MemLp (λ a, ∑ i ∈ s, f i a) p μ$$

Lean4

theorem memLp_finset_sum [ContinuousAdd ε'] {ι} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
    MemLp (fun a => ∑ i ∈ s, f i a) p μ :=
  by
  haveI : DecidableEq ι := Classical.decEq _
  revert hf
  refine Finset.induction_on s ?_ ?_
  · simp only [MemLp.zero', Finset.sum_empty, imp_true_iff]
  · intro i s his ih hf
    simp only [his, Finset.sum_insert, not_false_iff]
    exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Похожие утверждения