Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.forest_operator_g

Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:829 to 840

Source documentation

The g side of Proposition 2.0.4.

Exact Lean statement

lemma forest_operator_g (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‖ₑ ≤
    G2_0_4 a n * eLpNorm f 2 volume * eLpNorm g 2 volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma forest_operator_g (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‖ₑ ≤    G2_0_4 a n * eLpNorm f 2 volume * eLpNorm g 2 volume := by  calc    _ ≤ _ := forest_operator_g_prelude hf h2f hg h2g    _ ≤ _ := by      rw [mul_comm _ (eLpNorm f 2 volume), mul_assoc]; gcongr      rw [← ENNReal.rpow_le_rpow_iff (show (0 : ℝ) < (2 : ℕ) by norm_num),        ENNReal.rpow_natCast, ENNReal.rpow_natCast]      exact forest_operator_g_main hg h2g