Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.forest_operator_f

Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:990 to 1002

Source documentation

The f side of Proposition 2.0.4.

Exact Lean statement

lemma forest_operator_f (t : Forest X n)
    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ x, conj (g x) * ∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ ≤
    C2_0_4_aux a * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ *
    eLpNorm f 2 volume * eLpNorm g 2 volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma forest_operator_f (t : Forest X n)    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ x, conj (g x) * ∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ ≤    C2_0_4_aux a * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ *    eLpNorm f 2 volume * eLpNorm g 2 volume := by  calc    _ ≤ _ := forest_operator_f_prelude hf h2f hg h2g    _ ≤ _ := by      rw [← mul_rotate, mul_assoc]; gcongr      rw [← ENNReal.rpow_le_rpow_iff (show (0 : ℝ) < (2 : ℕ) by norm_num),        ENNReal.rpow_natCast, ENNReal.rpow_natCast]      exact forest_operator_f_main hf h2f