OneStepSchauderFlux

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

The flux-vanishing crux and the mean value property

The three files merged here close the chain from harmonicity to the mean value property:

• flux vanishing — for u harmonic on a neighbourhood of closedBall x R the spherical flux ∫_{∂B_r} ∂_ν u vanishes for every r < R, obtained by testing the weak Laplacian identity against a radial cutoff and using the polar decomposition;
• flux integration by parts — the derivative of the sphere average is the normalized flux;
• flux zero ⇒ constant sphere average, and hence the mean value property u(x) = ⨍_{∂B_r} u, in the exact form the reproducing convolution needs.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_radialTest_apply {d : ℕ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) (ξ : ↑(Metric.sphere 0 1)) : Laplacian.laplacian (fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) (x + r • ↑ξ) = 4 * r ^ 2 * deriv (deriv φ) (r ^ 2) + 2 * ↑d * deriv φ (r ^ 2)

Radiality of the test Laplacian on the sphere. For the radial test ψ(w) = φ(‖w − x‖²) with φ ∈ C^∞, the Laplacian evaluated at the sphere point x + r • ξ (ξ a unit vector, r > 0) equals the radial profile m(r) = 4 r² φ''(r²) + 2 d φ'(r²), independently of the direction ξ.

This is the radiality fact (from RadialLaplacian.laplacian_radial) that lets the polar bridge pull m(r) out of the sphere integral.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_sphere_eq_measureReal_smul_sphereAverage {d : ℕ} [NeZero d] (u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) : ∫ (ξ : ↑(Metric.sphere 0 1)), u (x + r • ↑ξ) ∂sphereMeasure d = (sphereMeasure d).real Set.univ • sphereAverage x r u

The un-normalized spherical integral is the measure times the normalized average. ∫_S u(x + r ξ) dσ(ξ) = σ(S) · sphereAverage x r u, from the definition of sphereAverage as the measure average ⨍.

Support of the Laplacian (helpers, re-derived natively)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_zero_fun' {d : ℕ} : Laplacian.laplacian 0 = 0

The Laplacian of the zero real-valued function vanishes.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.support_laplacian_subset' {d : ℕ} {ψ : EuclideanSpace ℝ (Fin d) → ℝ} : Function.support (Laplacian.laplacian ψ) ⊆ tsupport ψ

A function's Laplacian is supported in its topological support.

The radial weak identity — polar reduction of ∫ u · Δψ = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_Ioi_weighted_sphereAverage_eq_zero {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hψsupp : HasCompactSupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) {r : ℝ} (hr : 0 < r) (hrR : r < R) (htsupp : (tsupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) ⊆ Metric.ball x r) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (d - 1) * (4 * s ^ 2 * deriv (deriv φ) (s ^ 2) + 2 * ↑d * deriv φ (s ^ 2)) * sphereAverage x s u = 0

Radial weak identity. For u harmonic on Metric.ball x R (and globally C²) and a radial test ψ(w) = φ(‖w − x‖²) (φ ∈ C^∞, compactly supported inside Metric.ball x r, 0 < r < R), the local weak identity ∫ u · Δψ = 0 (CutoffLocalize) reduces, via the general polar bridge (piece 2) and the radial Laplacian profile (piece 1), to the one-dimensional vanishing ∫₀^∞ s^{d−1} · (4 s² φ''(s²) + 2 d φ'(s²)) · sphereAverage x s u ds = 0.

This is the entry point of the du Bois-Reymond endgame: the integrand's weight s^{d−1} · (4 s² φ''(s²) + 2 d φ'(s²)) is the total derivative (s^{d−1} p'(s))' (RadialLaplacian.hasDerivAt_weighted_radialProfile), so integrating by parts against sphereAverage x s u transfers onto its radial derivative ‖S‖⁻¹ · sphereFlux.

Support helpers

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.intervalIntegral_eq_integral_Ioi_of_zero {f : ℝ → ℝ} {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hint : MeasureTheory.Integrable f MeasureTheory.volume) (hzero : ∀ (s : ℝ), r < s → f s = 0) : ∫ (s : ℝ) in 0..R, f s = ∫ (s : ℝ) in Set.Ioi 0, f s

An integrable f that vanishes for s > r (with 0 < r < R) has the same integral over (0, ∞) and over the interval [0, R].

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialTest_eq_zero_of_ge {d : ℕ} [NeZero d] {φ : ℝ → ℝ} {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (htsupp : (tsupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) ⊆ Metric.ball x r) {t : ℝ} (ht : 0 ≤ t) (htr : r ^ 2 ≤ t) : φ t = 0

The radial profile of the test vanishes past r. If tsupport (φ(‖· − x‖²)) ⊆ ball x r, then φ t = 0 for every t ≥ r² (and t ≥ 0): otherwise a sphere point at radius √t ≥ r would lie in the support.

The flux test identity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_Ioi_test_sphereFlux_eq_zero {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hψsupp : HasCompactSupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) {r : ℝ} (hr : 0 < r) (hrR : r < R) (htsupp : (tsupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) ⊆ Metric.ball x r) : ∫ (s : ℝ) in Set.Ioi 0, 2 * s * deriv φ (s ^ 2) * (s ^ (d - 1) * sphereFlux x s u) = 0

Flux test identity (integration by parts). For u ∈ C² harmonic on Metric.ball x R and a radial test ψ = φ(‖· − x‖²) (φ ∈ C^∞, compactly supported inside Metric.ball x r, 0 < r < R), ∫₀^∞ (2 s φ'(s²)) · (s^{d−1} · sphereFlux x s u) ds = 0.

This is RadialLaplacian.hasDerivAt_weighted_radialProfile integrated by parts against sphereAverage, whose radial derivative is ‖S‖⁻¹ · sphereFlux. The test η(s) = 2 s φ'(s²) ranges over C^∞_c((0, R)) as φ ranges over admissible radial profiles, so this is the pairing consumed by the fundamental lemma.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereFlux_eq_zero_of_harmonic {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) {ρ : ℝ} (hρ0 : 0 < ρ) (hρR : ρ < R) : sphereFlux x ρ u = 0

Flux vanishing for harmonic functions. If u ∈ C² is harmonic on Metric.ball x R, then the average radial flux sphereFlux x ρ u vanishes for every ρ ∈ (0, R).

Proof by the monotone-cutoff contradiction described in the module docstring: a decreasing smooth radial cutoff makes the flux test identity's integrand single-signed, forcing the radial average of u to be locally constant across ρ, which is only consistent with zero flux.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_eq_center_of_harmonic {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) (r : ℝ) : r ∈ Set.Ico 0 R → sphereAverage x r u = u x

Spherical mean value property for harmonic functions. If u ∈ C² is harmonic on Metric.ball x R, then its spherical average about x equals the center value at every radius in [0, R): sphereAverage x r u = u x.