Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_inter_add_inter_compl

Carleson.Operators · Carleson/Operators.lean:170 to 178

Mathematical statement

Exact Lean statement

lemma carlesonSum_inter_add_inter_compl {f : X → ℂ} {x : X} (A B : Set (𝔓 X)) :
    carlesonSum (A ∩ B) f x + carlesonSum (A ∩ Bᶜ) f x = carlesonSum A f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_inter_add_inter_compl {f : X → ℂ} {x : X} (A B : Set (𝔓 X)) :    carlesonSum (A ∩ B) f x + carlesonSum (A ∩ Bᶜ) f x = carlesonSum A f x := by  classical  simp only [carlesonSum]  conv_rhs => rw [← Finset.sum_filter_add_sum_filter_not _ (fun p ↦ p ∈ B)]  congr 2  · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_inter_iff]  · ext; simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_inter_iff,      Set.mem_compl_iff]