Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_𝔓pos_inter_ℭ_eq_add_sum

Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:650 to 675

Source documentation

In each set ℭ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over various ℭ₁ k n j.

Exact Lean statement

lemma carlesonSum_𝔓pos_inter_ℭ_eq_add_sum {f : X → ℂ} {x : X} (hkn : k ≤ n) :
    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ k n) f x =
      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀ k n) f x
      + ∑ j ≤ 2 * n + 3, carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₁ k n j) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_𝔓pos_inter_ℭ_eq_add_sum {f : X → ℂ} {x : X} (hkn : k ≤ n) :    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ k n) f x =      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀ k n) f x      + ∑ j ≤ 2 * n + 3, carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₁ k n j) f x := by  conv_lhs => rw [← carlesonSum_inter_add_inter_compl _ (𝔏₀ k n)]  rw [sum_carlesonSum_of_pairwiseDisjoint]; swap  · apply PairwiseDisjoint.subset _ (subset_univ _)    apply (pairwiseDisjoint_ℭ₁ (k := k) (n := n)).mono    intro j    exact inter_subset_right  congr 2  · ext p    simp only [mem_inter_iff, mem_compl_iff, and_congr_left_iff, and_iff_left_iff_imp, and_imp]    intro hp    exact fun _ _ ↦ mem_of_mem_inter_left hp  · apply Subset.antisymm    · rintro p ⟨⟨hp, Hp⟩, h'p⟩      rcases exists_j_of_mem_𝔓pos_ℭ hp.1 Hp hkn with H      simp only [mem_compl_iff] at h'p      simp only [h'p, false_or] at H      simp only [Finset.mem_Iic, mem_iUnion, mem_inter_iff, hp, true_and, exists_prop]      exact H    · intro p hp      simp only [Finset.mem_Iic, mem_iUnion, exists_prop] at hp      rcases hp with ⟨i, hi, h'i, h''i⟩      exact ⟨⟨h'i, ℭ₁_subset_ℭ h''i⟩, disjoint_left.1 𝔏₀_disjoint_ℭ₁.symm h''i⟩