HarmonicBallMeanValue

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Ball and radial-moment bookkeeping for the mean value property on Vec d

HarmonicMeanValue proves the mean value property in kernel form: the pairing of a harmonic function against a continuous radial density supported in an annulus [a, b] of positive radial moment reproduces u z times the mass of the density. That statement avoids surface measure, the coarea formula and polar decomposition entirely, and it is stated for a weight rather than for the normalized indicator of a ball.

This module collects the two elementary facts a caller of that kernel form needs before it can be read at an explicit Euclidean ball: the ball has finite Lebesgue measure, and a density that is merely positive on a subinterval of its support already has positive radial moment, which is the shape in which the kernel hypothesis is usually verified.

No coarea formula, no surface measure and no polar decomposition is used, and no EuclideanSpace transfer appears anywhere: everything stays on Vec d with the explicit Euclidean balls.

Contents

• volume_euclideanBall_ne_top -- an explicit Euclidean ball has finite Lebesgue measure.
• radialMoment_pos_of_pos_on -- positivity of a radial moment from positivity on a subinterval.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.volume_euclideanBall_ne_top {d : ℕ} (z : HCPolySupport.Vec d) (ρ : ℝ) : MeasureTheory.volume (HCPolySupport.euclideanBall z ρ) ≠ ⊤

Explicit Euclidean balls have finite Lebesgue measure.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_pos_of_pos_on {m : ℕ} {k : ℝ → ℝ} (hk : Continuous k) (hknn : ∀ (t : ℝ), 0 ≤ k t) {p q b : ℝ} (hp : 0 < p) (hpq : p < q) (hqb : q ≤ b) (hpos : ∀ (t : ℝ), p < t → t < q → 0 < k t) : 0 < radialMoment m k b

Positivity of the radial moment from positivity on a subinterval.