A dimensional r³ localization estimate, derived from the interior bound.

noncomputable def EulerMeanHarmonic.harmonicSmallBallConstant : ℝ

Harmonic small ball constant, given by (Real.pi * 4 / 3) * harmonicInteriorConstant ^ 2.

Equations

• EulerMeanHarmonic.harmonicSmallBallConstant = Real.pi * 4 / 3 * EulerMeanHarmonic.harmonicInteriorConstant ^ 2

theorem EulerMeanHarmonic.harmonicSmallBallConstant_nonneg : 0 ≤ harmonicSmallBallConstant

theorem EulerMeanHarmonic.volume_ball_toReal (r : ℝ) (hr : 0 ≤ r) : (MeasureTheory.volume (Metric.ball 0 r)).toReal = r ^ 3 * (Real.pi * 4 / 3)

theorem EulerMeanHarmonic.harmonic_smallBall_energy (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (r : ℝ) (hr : 0 ≤ r) (hrhalf : r ≤ 1 / 2) : ∫ (x : EulerSmoothLimit.Space) in Metric.ball 0 r, h x ^ 2 ≤ harmonicSmallBallConstant * r ^ 3 * MeasureTheory.lpNorm h 2 MeasureTheory.volume ^ 2

The mass on a ball of radius r is bounded by r³ times the global L² mass.