Source indexedlemma · leanprover/lean4:v4.32.0

lintegral_carlesonSum_forest

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:752 to 791

Source documentation

For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁.

Exact Lean statement

lemma lintegral_carlesonSum_forest
    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ ≤
    C2_0_4 a q n * (2 ^ (2 * a + 5) * volume F / volume G) ^ (q⁻¹ - 2⁻¹) *
    (volume F) ^ (1/2 : ℝ) * (volume G) ^ (1/2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lintegral_carlesonSum_forest    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ ≤    C2_0_4 a q n * (2 ^ (2 * a + 5) * volume F / volume G) ^ (q⁻¹ - 2⁻¹) *    (volume F) ^ (1/2 : ℝ) * (volume G) ^ (1/2 : ℝ) := by  classical  let 𝔉 := forest (X := X) k n j l  have : ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ =      ∫⁻ x in G \ G', ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ₑ := by    congr with x    congr    rw [sum_carlesonSum_of_pairwiseDisjoint]; swap    · intro a ha b hb hab      simp only [Function.onFun, disjoint_iff_forall_ne]      intro x hx y hy      simp only [Finset.coe_filter, Finset.mem_univ, true_and, 𝔉] at ha hb hx hy      have := forest_disjoint (X := X) (𝔘₄_subset_𝔘₃ ha) (𝔘₄_subset_𝔘₃ hb) hab      exact disjoint_iff_forall_ne.1 this hx hy    congr with p    simp_rw [mem_iUnion, exists_prop, Finset.mem_filter_univ]    exact Iff.rfl  rw [this]  have W := forest_operator_le_volume 𝔉 hf h2f (A := G \ G')    (measurableSet_G.diff measurable_G') sdiff_subset  apply W.trans  gcongr  · simp only [sub_nonneg, inv_le_inv₀ zero_lt_two (q_pos X)]    exact (q_mem_Ioc (X := X)).2  · rw [dens₂_eq_biSup_dens₂]    simp only [mem_iUnion, exists_prop, iSup_exists, iSup_le_iff, and_imp]    intro p q hq hp    replace hp : p ∈ ℭ₆ k n j := 𝔗₂_subset_ℭ₆ hp    have : ¬ (𝓘 p : Set X) ⊆ G₁ := by      have W := hp.2      contrapose! W      exact W.trans (subset_union_left.trans subset_union_left)    contrapose! this    change p ∈ highDensityTiles at this    apply subset_biUnion_of_mem this  · exact sdiff_subset