BallAverage #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Value at a centre from an L² bound and a Hölder modulus #
A continuous representative whose oscillation on a ball is controlled by a
Hölder modulus has its value at the centre controlled by the L² average of
the function on that ball plus the modulus. This is the step that converts an
L² smallness statement into a pointwise one.
Main results #
theorem
DivergenceFormProcess.Decay.integral_abs_le_sqrt_mul_sqrt
{d : ℕ}
{mu : MeasureTheory.Measure (HCPolySupport.Vec d)}
[MeasureTheory.IsFiniteMeasure mu]
{w : HCPolySupport.Vec d → ℝ}
(hw : MeasureTheory.Integrable w mu)
(hw2 : MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => w y ^ 2) mu)
:
Cauchy--Schwarz against the constant one, in the elementary Young form.
theorem
DivergenceFormProcess.Decay.abs_center_le_of_holder
{d : ℕ}
[NeZero d]
{x₀ : HCPolySupport.Vec d}
{rho K alpha : ℝ}
(hrho : 0 < rho)
{v w : HCPolySupport.Vec d → ℝ}
(hHolder : ∀ y ∈ HCPolySupport.euclideanBall x₀ rho, |v x₀ - v y| ≤ K * rho ^ alpha)
(hae : v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ rho)] w)
(hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ rho)))
:
|v x₀| ≤ √(∫ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x₀ rho, w y ^ 2) / √((MeasureTheory.volume
(Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d)).toReal * rho ^ d) + K * rho ^ alpha
The value of a continuous representative at the centre of a ball is bounded
by the L² average of an almost-everywhere equal function plus the Hölder
modulus on that ball.