Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.adjoint_tree_estimate

Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:132 to 143

Source documentation

Part 1 of Lemma 7.4.2.

Exact Lean statement

lemma adjoint_tree_estimate
    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :
    eLpNorm (adjointCarlesonSum (t u) g) 2 volume ≤
    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma adjoint_tree_estimate    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :    eLpNorm (adjointCarlesonSum (t u) g) 2 volume ≤    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 volume := by  by_cases h : eLpNorm (adjointCarlesonSum (t u) g) 2 = 0  · rw [h]; exact zero_le  have bcs : BoundedCompactSupport (adjointCarlesonSum (t u) g) := hg.adjointCarlesonSum  rw [← ENNReal.mul_le_mul_iff_left h (bcs.memLp 2).eLpNorm_ne_top, ← sq,    eLpNorm_two_eq_enorm_integral_mul_conj (bcs.memLp 2), mul_assoc _ (eLpNorm g 2 volume),    mul_comm (eLpNorm g 2 volume), ← mul_assoc]  conv_lhs => enter [1, 2, x]; rw [mul_comm]  exact adjoint_density_tree_bound1 bcs hg h2g hu