HarmonicMeanValue

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

The mean value property for the coordinate Laplacian on Vec d

Mathlib proves the mean value property for harmonic functions only in the complex plane (Analysis/Complex/Harmonic/MeanValue, through circleAverage); it has no sphereAverage at all, and its harmonic layer is stated for InnerProductSpace R E, which the sup-normed carrier Vec d does not satisfy. CoarseGraining has no mean value property either. This module supplies one natively for CoarseGraining's coordinate Laplacian on Vec d, in the kernel form that avoids surface measure entirely.

The argument is the classical one, run through the Green pairing of HarmonicGreen rather than through the divergence theorem:

1. Zero moment kills the pairing. If a continuous radial density k is supported in an annulus [a, b] with 0 < a < b and its radial moment int_0^b s^(d-1) k s ds vanishes, then HarmonicSphereBump produces a compactly supported C^2 function psi with Delta psi = k(|· - z|), and Green's second identity gives int u (x) k (|x - z|) dx = 0 for every u that is C^2 and harmonic on the closed ball of radius b. Taking u = 1 -- itself harmonic -- gives the same statement for the mass of the density.
2. Kernel independence. Applying step 1 to the combination M_2 k_1 - M_1 k_2 of two densities with moments M_1, M_2 shows that M_2 * int u k_1 = M_1 * int u k_2, and likewise for the masses. Hence the normalized pairing int u k / int k does not depend on the density.
3. Concentration. For a nonnegative density supported in the ball of radius delta, the normalized pairing differs from u z by at most the oscillation of u on that ball. Shrinking delta and using continuity of u pins the common value of step 2 to u z.

No surface measure, no coarea formula and no polar decomposition are used: the whole argument stays inside the Green pairing. The explicit density annulusBump a b t = max 0 ((t - a) * (b - t)) makes the final statement unconditional.

Contents

• integral_mul_radial_eq_zero_of_radialMoment_eq_zero -- step 1.
• integral_radial_eq_zero_of_radialMoment_eq_zero -- step 1 with u = 1.
• radialMoment_mul_integral_comm -- step 2.
• abs_integral_mul_radial_sub_le -- step 3.
• integral_mul_radial_eq_mul_integral_of_harmonic -- the mean value property in kernel form: int u (x) k (|x - z|) dx = u z * int k (|x - z|) dx.
• annulusBump, annulusBump_pos, radialMoment_annulusBump_pos and integral_radial_pos -- the explicit density, its positivity on the open annulus, the positivity of its radial moment, and the positivity of the mass of any such radial density in every dimension d >= 1. Dividing the kernel form by that mass is the normalized mean value property.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordLaplacian_const {d : ℕ} (c : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.euclideanCoordLaplacian (fun (x : HCPolySupport.Vec d) => c) x = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_comp_euclideanNorm_sub {m : ℕ} {k : ℝ → ℝ} (hk : Continuous k) (z : HCPolySupport.Vec (m + 1)) : Continuous fun (x : HCPolySupport.Vec (m + 1)) => k (euclideanNorm (x - z))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasCompactSupport_mul_radial {m : ℕ} {k : ℝ → ℝ} {b : ℝ} {u : HCPolySupport.Vec (m + 1) → ℝ} (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (z : HCPolySupport.Vec (m + 1)) : HasCompactSupport fun (x : HCPolySupport.Vec (m + 1)) => u x * k (euclideanNorm (x - z))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrable_mul_radial {m : ℕ} {k : ℝ → ℝ} {b : ℝ} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : Continuous u) (hk : Continuous k) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (z : HCPolySupport.Vec (m + 1)) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec (m + 1)) => u x * k (euclideanNorm (x - z))) MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrable_radial {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (z : HCPolySupport.Vec (m + 1)) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec (m + 1)) => k (euclideanNorm (x - z))) MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_radial_eq_zero_of_radialMoment_eq_zero {m : ℕ} {k : ℝ → ℝ} {a b : ℝ} {z : HCPolySupport.Vec (m + 1)} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : ContDiff ℝ (↑2) u) (hk : Continuous k) (ha : 0 < a) (hb : 0 < b) (hk0 : ∀ s ≤ a, k s = 0) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) (hharm : ∀ x ∈ HCPolySupport.euclideanClosedBall z b, HCPolySupport.euclideanCoordLaplacian u x = 0) : ∫ (x : HCPolySupport.Vec (m + 1)), u x * k (euclideanNorm (x - z)) = 0

Vanishing of the Green pairing against a radial density of zero moment.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_radial_eq_zero_of_radialMoment_eq_zero {m : ℕ} {k : ℝ → ℝ} {a b : ℝ} (hk : Continuous k) (ha : 0 < a) (hb : 0 < b) (hk0 : ∀ s ≤ a, k s = 0) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) (z : HCPolySupport.Vec (m + 1)) : ∫ (x : HCPolySupport.Vec (m + 1)), k (euclideanNorm (x - z)) = 0

The u = 1 case: a radial density of zero moment integrates to zero.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_linear {m : ℕ} {k₁ k₂ : ℝ → ℝ} (hk₁ : Continuous k₁) (hk₂ : Continuous k₂) (c₁ c₂ t : ℝ) : radialMoment m (fun (s : ℝ) => c₁ * k₁ s + c₂ * k₂ s) t = c₁ * radialMoment m k₁ t + c₂ * radialMoment m k₂ t

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump (a b t : ℝ) : ℝ

The explicit continuous annulus bump supported in [a, b].

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump a b t = max 0 ((t - a) * (b - t))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_annulusBump (a b : ℝ) : Continuous (annulusBump a b)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump_nonneg (a b t : ℝ) : 0 ≤ annulusBump a b t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump_eq_zero_of_le {a b : ℝ} (hab : a < b) {t : ℝ} (ht : t ≤ a) : annulusBump a b t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump_eq_zero_of_ge {a b : ℝ} (hab : a < b) {t : ℝ} (ht : b ≤ t) : annulusBump a b t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusBump_pos {a b t : ℝ} (h1 : a < t) (h2 : t < b) : 0 < annulusBump a b t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_annulusBump_pos {m : ℕ} {a b : ℝ} (ha : 0 < a) (hab : a < b) : 0 < radialMoment m (annulusBump a b) b

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm_smul_basisVec {d : ℕ} (c : ℝ) (i : Fin d) : euclideanNorm (c • HCPolySupport.basisVec i) = |c|

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_radial_pos {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hknn : ∀ (t : ℝ), 0 ≤ k t) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) {t₀ : ℝ} (ht₀ : 0 ≤ t₀) (hkt₀ : 0 < k t₀) (z : HCPolySupport.Vec (m + 1)) : 0 < ∫ (x : HCPolySupport.Vec (m + 1)), k (euclideanNorm (x - z))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_mul_integral_comm {m : ℕ} {b : ℝ} {z : HCPolySupport.Vec (m + 1)} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : ContDiff ℝ (↑2) u) {k₁ k₂ : ℝ → ℝ} (hk₁ : Continuous k₁) (hk₂ : Continuous k₂) {a₁ a₂ : ℝ} (ha₁ : 0 < a₁) (ha₂ : 0 < a₂) (hb : 0 < b) (hk₁0 : ∀ s ≤ a₁, k₁ s = 0) (hk₁b : ∀ (s : ℝ), b ≤ s → k₁ s = 0) (hk₂0 : ∀ s ≤ a₂, k₂ s = 0) (hk₂b : ∀ (s : ℝ), b ≤ s → k₂ s = 0) (hharm : ∀ x ∈ HCPolySupport.euclideanClosedBall z b, HCPolySupport.euclideanCoordLaplacian u x = 0) : radialMoment m k₂ b * ∫ (x : HCPolySupport.Vec (m + 1)), u x * k₁ (euclideanNorm (x - z)) = radialMoment m k₁ b * ∫ (x : HCPolySupport.Vec (m + 1)), u x * k₂ (euclideanNorm (x - z))

Kernel independence. For a function harmonic on the closed ball of radius b, the pairing against a radial density is proportional to the density's radial moment, with a proportionality factor that does not depend on the density.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.abs_integral_mul_radial_sub_le {m : ℕ} {k : ℝ → ℝ} {b : ℝ} {z : HCPolySupport.Vec (m + 1)} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : Continuous u) (hk : Continuous k) (hknn : ∀ (t : ℝ), 0 ≤ k t) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) {ε : ℝ} (hε : ∀ x ∈ HCPolySupport.euclideanClosedBall z b, |u x - u z| ≤ ε) : |(∫ (x : HCPolySupport.Vec (m + 1)), u x * k (euclideanNorm (x - z))) - u z * ∫ (x : HCPolySupport.Vec (m + 1)), k (euclideanNorm (x - z))| ≤ ε * ∫ (x : HCPolySupport.Vec (m + 1)), k (euclideanNorm (x - z))

Concentration. A nonnegative radial density supported in the ball of radius b reproduces the value at the centre up to the oscillation of u on that ball.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_radial_eq_mul_integral_of_harmonic {m : ℕ} {k : ℝ → ℝ} {a b : ℝ} {z : HCPolySupport.Vec (m + 1)} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : ContDiff ℝ (↑2) u) (hk : Continuous k) (ha : 0 < a) (hab : a < b) (hk0 : ∀ s ≤ a, k s = 0) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : 0 < radialMoment m k b) (hharm : ∀ x ∈ HCPolySupport.euclideanClosedBall z b, HCPolySupport.euclideanCoordLaplacian u x = 0) : ∫ (x : HCPolySupport.Vec (m + 1)), u x * k (euclideanNorm (x - z)) = u z * ∫ (x : HCPolySupport.Vec (m + 1)), k (euclideanNorm (x - z))

The mean value property, in kernel form. If u is C^2 with vanishing coordinate Laplacian on the closed Euclidean ball of radius b about z, then its pairing against any nonnegative continuous radial density supported in the annulus [a, b] of positive radial moment is u z times the mass of the density.