Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.MemLp.maximalFunction_lt_top

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:189 to 197

Mathematical statement

Exact Lean statement

theorem MeasureTheory.MemLp.maximalFunction_lt_top (hp₁ : 0 < p) (hu : MemLp u ⊤ μ) :
    maximalFunction μ 𝓑 c r p u x < ∞

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem MeasureTheory.MemLp.maximalFunction_lt_top (hp₁ : 0 < p) (hu : MemLp u ⊤ μ) :    maximalFunction μ 𝓑 c r p u x < ∞ := by  rw [maximalFunction_eq_maximalFunction_one_rpow (by positivity)]  apply rpow_lt_top_of_nonneg (by positivity) (lt_top_iff_ne_top.mp _)  have : MemLp (fun x ↦ ‖u x‖ ^ p) ⊤ μ := by    rw [← toReal_ofReal hp₁.le,      show ∞ = ∞ / (ENNReal.ofReal p) from ENNReal.top_div_of_ne_top (by finiteness) |>.symm]    exact hu.norm_rpow_div _  refine lt_of_le_of_lt maximalFunction_one_le_eLpNormEssSup this.eLpNormEssSup_lt_top