Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_𝔓pos_inter_𝔏₀_eq_sum

Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:677 to 689

Mathematical statement

Exact Lean statement

lemma carlesonSum_𝔓pos_inter_𝔏₀_eq_sum {f : X → ℂ} {x : X} :
    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀ k n) f x =
      ∑ l < n, carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀' k n l) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_𝔓pos_inter_𝔏₀_eq_sum {f : X → ℂ} {x : X} :    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀ k n) f x =      ∑ l < n, carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀' k n l) f x := by  rw [sum_carlesonSum_of_pairwiseDisjoint]; swap  · apply PairwiseDisjoint.subset _ (subset_univ _)    apply (pairwiseDisjoint_L0' (k := k) (n := n)).mono    intro j    exact inter_subset_right  congr  rw [← iUnion_L0']  ext p  simp only [mem_inter_iff, mem_iUnion, Finset.mem_Iio]  tauto