Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_ℭ₅_eq_ℭ₆

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:714 to 730

Source documentation

The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G'.

Exact Lean statement

lemma carlesonSum_ℭ₅_eq_ℭ₆ {f : X → ℂ} {x : X} (hx : x ∈ G \ G') {k n j : ℕ} :
    carlesonSum (ℭ₅ k n j) f x = carlesonSum (ℭ₆ k n j) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_ℭ₅_eq_ℭ₆ {f : X → ℂ} {x : X} (hx : x ∈ G \ G') {k n j : ℕ} :    carlesonSum (ℭ₅ k n j) f x = carlesonSum (ℭ₆ k n j) f x := by  classical  simp only [carlesonSum]  symm  apply Finset.sum_subset  · intro p hp    rw [Finset.mem_filter_univ] at hp ⊢    exact ℭ₆_subset_ℭ₅ hp  · intro p hp h'p    rw [Finset.mem_filter_univ] at hp h'p    have : x ∉ 𝓘 p := by      simp only [ℭ₆, mem_setOf_eq, not_and, Decidable.not_not] at h'p      intro h'x      exact hx.2 (h'p hp h'x)    have : x ∉ E p := by simp at this; simp [E, this]    simp [carlesonOn, this]