Source indexedlemma · leanprover/lean4:v4.32.0

hasStrongType_maximalFunction_one

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:268 to 286

Source documentation

Special case of equation (2.0.44). The proof is given between (9.0.12) and (9.0.34). Use the real interpolation theorem instead of following the blueprint.

Exact Lean statement

public lemma hasStrongType_maximalFunction_one [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E]
    [BorelSpace E] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure]
    {p : ℝ≥0} (hp : 1 < p) :
    HasStrongType (maximalFunction (E := E) μ 𝓑 c r 1) p p μ μ (CMB A p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

public lemma hasStrongType_maximalFunction_one [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E]    [BorelSpace E] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure]    {p : ℝ≥0} (hp : 1 < p) :    HasStrongType (maximalFunction (E := E) μ 𝓑 c r 1) p p μ μ (CMB A p) := by  by_cases h : Nonempty X; swap  · have := not_nonempty_iff.mp h; intro _ _; simp  rw [CMB]  refine exists_hasStrongType_real_interpolation    (T := maximalFunction (E := E) μ 𝓑 c r 1) (p := p) (q := p) (A := 1) (t := (↑p)⁻¹)    ⟨ENNReal.zero_lt_top, le_rfl⟩    ⟨zero_lt_one, le_rfl⟩ (by norm_num) le_rfl ?_    zero_lt_one (pow_pos (A_pos μ) 2)    (by simp) (by simp)    (fun f _ ↦ measurable_maximalFunction.aestronglyMeasurable)    ?_ (hasStrongType_maximalFunction_top |>.hasWeakType zero_lt_top)    hasWeakType_maximalFunction_one  · exact ⟨ENNReal.inv_pos.mpr coe_ne_top, ENNReal.inv_lt_one.mpr <| one_lt_coe_iff.mpr hp⟩  exact sublinearOn_maximalFunction_one.imp (·.elim (·.aemeasurable) (·.aemeasurable))    |>.aeSublinearOn.1