Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_ℭ₆_eq_sum

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:734 to 748

Source documentation

The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests based on 𝔘₄ k n j l.

Exact Lean statement

lemma carlesonSum_ℭ₆_eq_sum {f : X → ℂ} {x : X} {k n j : ℕ} (hkn : k ≤ n) :
    carlesonSum (ℭ₆ k n j) f x =
      ∑ l < 4 * n + 12, carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_ℭ₆_eq_sum {f : X → ℂ} {x : X} {k n j : ℕ} (hkn : k ≤ n) :    carlesonSum (ℭ₆ k n j) f x =      ∑ l < 4 * n + 12, carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x := by  rw [sum_carlesonSum_of_pairwiseDisjoint]; swap  · intro a ha b hb hab    simp only [Function.onFun, disjoint_iff_forall_ne, mem_iUnion, exists_prop, ne_eq,      forall_exists_index, and_imp]    intro q p hp hq q' p' hp' hq'    have := pairwiseDisjoint_𝔘₄ (X := X) (k := k) (n := n) (j := j) (mem_univ a) (mem_univ b) hab    have : p ≠ p' := disjoint_iff_forall_ne.1 this hp hp'    have := forest_disjoint (𝔘₄_subset_𝔘₃ hp) (𝔘₄_subset_𝔘₃ hp') this    exact disjoint_iff_forall_ne.1 this hq hq'  congr  ext p  simp only [C6_forest' hkn, mem_Iio, mem_iUnion, exists_prop, Finset.mem_Iio]