Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.indicator_adjoint_tree_estimate

Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:154 to 171

Source documentation

Part 2 of Lemma 7.4.2.

Exact Lean statement

lemma indicator_adjoint_tree_estimate
    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :
    eLpNorm (F.indicator (adjointCarlesonSum (t u) g)) 2 ≤
    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma indicator_adjoint_tree_estimate    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :    eLpNorm (F.indicator (adjointCarlesonSum (t u) g)) 2 ≤    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 := by  by_cases h : eLpNorm (F.indicator (adjointCarlesonSum (t u) g)) 2 = 0  · rw [h]; exact zero_le  have bcs : BoundedCompactSupport (F.indicator (adjointCarlesonSum (t u) g)) :=    hg.adjointCarlesonSum.indicator measurableSet_F  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]  calc    _ = ‖∫ x, conj (adjointCarlesonSum (t u) g x) *        F.indicator (adjointCarlesonSum (t u) g) x‖ₑ := by      congr 2 with x; nth_rw 2 [indicator_eq_indicator_one_mul]      rw [map_mul, conj_indicator, map_one, ← mul_assoc, mul_comm _ (F.indicator 1 x),        ← indicator_eq_indicator_one_mul, indicator_indicator, inter_self, mul_comm]    _ ≤ _ := adjoint_density_tree_bound2 bcs support_indicator_subset hg h2g hu