Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.density_tree_bound1

Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:460 to 468

Source documentation

First part of Lemma 7.3.1.

Exact Lean statement

lemma density_tree_bound1 (hf : BoundedCompactSupport f)
    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :
    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ ≤
    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma density_tree_bound1 (hf : BoundedCompactSupport f)    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ ≤    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by  have hc : eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume ≤ 1 * eLpNorm f 2 volume := by    have : ∀ L ∈ 𝓙 (t u), volume ((L : Set X) ∩ univ) ≤ 1 * volume (L : Set X) := by intros; simp    apply le_of_le_of_eq <| eLpNorm_approxOnCube_two_le pairwiseDisjoint_𝓙 .univ this hf (by tauto)    rw [ENNReal.one_rpow]  simpa using density_tree_bound_aux hf hg h2g hu hc