Source indexedlemma · leanprover/lean4:v4.32.0

rcarleson_general

Carleson.Classical.CarlesonOnTheRealLineContinuous · Carleson/Classical/CarlesonOnTheRealLineContinuous.lean:17 to 26

Mathematical statement

Exact Lean statement

lemma rcarleson_general {q q' : ℝ≥0} (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q')
    {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)
    (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    ∫⁻ x in G, T f x ≤ C10_0_1 4 q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rcarleson_general {q q' : ℝ≥0} (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q')    {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)    (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    ∫⁻ x in G, T f x ≤ C10_0_1 4 q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by  calc ∫⁻ x in G, T f x    _ ≤ ∫⁻ x in G, carlesonOperator K f x :=      lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)    _ ≤ C10_0_1 4 q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ :=      two_sided_metric_carleson (a := 4) (by norm_num) hq hqq' hF hG        Hilbert_strong_2_2 hmf hf