Source indexedtheorem · leanprover/lean4:v4.32.0

AEEqFun.mk_sum

Carleson.ToMathlib.MeasureTheory.Function.AEEqFun · Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean:11 to 22

Mathematical statement

Exact Lean statement

theorem AEEqFun.mk_sum {α E ι : Type*} {m0 : MeasurableSpace α}
    {μ : Measure α} [inst : NormedAddCommGroup E] {s : Finset ι} {f : ι → α → E}
    (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) :
      AEEqFun.mk (∑ i ∈ s, f i) (Finset.aestronglyMeasurable_sum s hf) =
      ∑ i ∈ s.attach, AEEqFun.mk (f ↑i) (hf i (Finset.coe_mem i))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem AEEqFun.mk_sum {α E ι : Type*} {m0 : MeasurableSpace α}    {μ : Measure α} [inst : NormedAddCommGroup E] {s : Finset ι} {f : ι → α → E}    (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) :      AEEqFun.mk (∑ i ∈ s, f i) (Finset.aestronglyMeasurable_sum s hf) =      ∑ i ∈ s.attach, AEEqFun.mk (f ↑i) (hf i (Finset.coe_mem i)) := by  classical  induction s using Finset.induction_on with  | empty => simp only [sum_empty, attach_empty]; rfl  | insert i s hi h =>    simp_rw [sum_insert hi]    have := fun i hi ↦ hf i (mem_insert_of_mem hi)    rw [sum_attach_insert hi, ← AEEqFun.mk_add_mk _ _ _ (aestronglyMeasurable_sum s this), h this]