Source indexedtheorem · leanprover/lean4:v4.32.0

lintegral_ball_le_volume_mul_globalMaximalFunction

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:45 to 53

Source documentation

The integral of the norm of a function over a particular ball is smaller than the volume of the ball times the value of the globalMaximalFuntion at a point inside that ball.

Exact Lean statement

public theorem lintegral_ball_le_volume_mul_globalMaximalFunction
    [ProperSpace X] [IsFiniteMeasureOnCompacts μ] {z : X} {r : ℝ}
    (h : dist x z < r) :
    ∫⁻ y in ball z r, ‖u y‖ₑ ∂μ ≤ μ (ball z r) * globalMaximalFunction μ 1 u x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

public theorem lintegral_ball_le_volume_mul_globalMaximalFunction    [ProperSpace X] [IsFiniteMeasureOnCompacts μ] {z : X} {r : ℝ}    (h : dist x z < r) :    ∫⁻ y in ball z r, ‖u y‖ₑ ∂μ ≤ μ (ball z r) * globalMaximalFunction μ 1 u x := by  have : IsFiniteMeasure (μ.restrict (ball z r)) := isFiniteMeasure_restrict.mpr (by finiteness)  rw [← measure_mul_laverage]  simp only [MeasurableSet.univ, Measure.restrict_apply, univ_inter]  gcongr  exact laverage_le_globalMaximalFunction h