FluxSubharmonic

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

Subharmonic extension of the spherical flux calculus

This module contains only the subharmonic additions to the paper-side spherical flux machinery. The harmonic definitions and mean-value lemmas are reused from OneStepSchauderFlux.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sphereMeasure_mul_integral_Ioi_weighted_sphereAverage_eq_laplacian {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hψsupp : HasCompactSupport fun (w : EuclideanSpace ℝ (Fin d)) => φ (‖w - x‖ ^ 2)) : (Section4.Provider.ExcessDecay.Schauder.sphereMeasure d).real Set.univ * ∫ (s : ℝ) in Set.Ioi 0, s ^ (d - 1) * (4 * s ^ 2 * deriv (deriv φ) (s ^ 2) + 2 * ↑d * deriv φ (s ^ 2)) * Section4.Provider.ExcessDecay.Schauder.sphereAverage x s u = ∫ (y : EuclideanSpace ℝ (Fin d)), Laplacian.laplacian u y * φ (‖y - x‖ ^ 2)

The flux test identity

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integral_Ioi_test_sphereFlux_eq_neg_integral_laplacian {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {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) * Section4.Provider.ExcessDecay.Schauder.sphereFlux x s u) = -∫ (y : EuclideanSpace ℝ (Fin d)), Laplacian.laplacian u y * φ (‖y - x‖ ^ 2)

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.StochasticProcess.Common.Regularity.Ported.sphereFlux_nonneg_of_laplacian_nonneg {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hlap : ∀ y ∈ Metric.ball x R, 0 ≤ Laplacian.laplacian u y) {ρ : ℝ} (hρ0 : 0 < ρ) (hρR : ρ < R) : 0 ≤ Section4.Provider.ExcessDecay.Schauder.sphereFlux x ρ u

Outward flux is nonnegative for a subharmonic function.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sphereAverage_mono_of_laplacian_nonneg {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hlap : ∀ y ∈ Metric.ball x R, 0 ≤ Laplacian.laplacian u y) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbR : b < R) : Section4.Provider.ExcessDecay.Schauder.sphereAverage x a u ≤ Section4.Provider.ExcessDecay.Schauder.sphereAverage x b u

Spherical averages of a smooth subharmonic function are nondecreasing in the radius.