add — Mathlib

English

If each f(i) belongs to ℓ^p, then the finite sum over a Finset also belongs to ℓ^p.

Русский

Если каждый f(i) принадлежит ℓ^p, то конечная сумма по Finset тоже принадлежит ℓ^p.

LaTeX

$$$$ \forall \iota \in \mathrm{Finset}, \; \text{Mem}_{\ell^p}\bigl(\sum_{i \in s} f_i, p\bigr). $$$$

Lean4

theorem add {f g : ∀ i, E i} (hf : Memℓp f p) (hg : Memℓp g p) : Memℓp (f + g) p :=
  by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_
    simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_setOf_eq]
    contrapose!
    rintro ⟨hf', hg'⟩
    simp [hf', hg']
  · apply memℓp_infty
    obtain ⟨A, hA⟩ := hf.bddAbove
    obtain ⟨B, hB⟩ := hg.bddAbove
    refine ⟨A + B, ?_⟩
    rintro a ⟨i, rfl⟩
    exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))
  apply memℓp_gen
  let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)
  refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)
  · intro; positivity
  · refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_
    dsimp only [C]
    split_ifs with h
    · simpa using NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)
    · let F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
      simp only [not_lt] at h
      simpa [Fin.sum_univ_succ] using
        Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

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