Source indexedlemma · leanprover/lean4:v4.32.0

sum_carlesonSum_of_pairwiseDisjoint

Carleson.Operators · Carleson/Operators.lean:180 to 199

Mathematical statement

Exact Lean statement

lemma sum_carlesonSum_of_pairwiseDisjoint {ι : Type*} {f : X → ℂ} {x : X} {A : ι → Set (𝔓 X)}
    {s : Finset ι} (hs : (s : Set ι).PairwiseDisjoint A) :
    ∑ i ∈ s, carlesonSum (A i) f x = carlesonSum (⋃ i ∈ s, A i) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_carlesonSum_of_pairwiseDisjoint {ι : Type*} {f : X → ℂ} {x : X} {A : ι → Set (𝔓 X)}    {s : Finset ι} (hs : (s : Set ι).PairwiseDisjoint A) :    ∑ i ∈ s, carlesonSum (A i) f x = carlesonSum (⋃ i ∈ s, A i) f x := by  classical  simp only [carlesonSum]  rw [← Finset.sum_biUnion]  · congr with p    simp only [Finset.mem_biUnion, Finset.mem_filter, Finset.mem_univ, true_and,      Set.mem_iUnion₂, exists_prop]  · convert hs    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩    · intro i hi j hj hij      convert! Finset.disjoint_coe.2 (h hi hj hij)      · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_coe]      · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_coe]    · intro i hi j hj hij      apply Finset.disjoint_coe.1      convert! h hi hj hij      · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_coe]      · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_coe]