HarmonicGradientSubmean

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

Submean structure of the energy of a harmonic gradient

This file supplies the smooth analytic half of the constant-one concentric-ball energy comparison used by the small-contrast Schauder iteration. It is kept on the coordinate carrier long enough to reuse the established mixed-derivative calculus, then transported to the Euclidean carrier used by the sphere/flux machinery.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ae_eq_euclideanGradient_of_ae_eq_of_contDiff {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVU : V ⊆ U) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (h : HCPolySupport.H1Function U) {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 1 v) (hae : v =ᵐ[MeasureTheory.volume.restrict V] h.toFun) : HCPolySupport.euclideanGradient v =ᵐ[MeasureTheory.volume.restrict V] h.grad

Identification of the gradient of a smooth representative with the weak gradient on an open subwindow.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.euclideanCoordLaplacian_euclideanCoordDeriv_eq_zero {d : ℕ} {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hharm : ∀ y ∈ U, HCPolySupport.euclideanCoordLaplacian u y = 0) {x : HCPolySupport.Vec d} (hx : x ∈ U) (i : Fin d) : HCPolySupport.euclideanCoordLaplacian (HCPolySupport.euclideanCoordDeriv i u) x = 0

A coordinate derivative of a smooth coordinate-harmonic function is coordinate-harmonic.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.euclideanCoordLaplacian_sq {d : ℕ} {g : HCPolySupport.Vec d → ℝ} (hg : ContDiff ℝ (↑⊤) g) (x : HCPolySupport.Vec d) : HCPolySupport.euclideanCoordLaplacian (fun (y : HCPolySupport.Vec d) => g y ^ 2) x = 2 * ∑ j : Fin d, HCPolySupport.euclideanCoordDeriv j g x ^ 2 + 2 * g x * HCPolySupport.euclideanCoordLaplacian g x

The coordinate Laplacian of a square is twice the squared coordinate gradient plus twice the function times its Laplacian.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.euclideanCoordLaplacian_sq_euclideanCoordDeriv_nonneg {d : ℕ} {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hharm : ∀ y ∈ U, HCPolySupport.euclideanCoordLaplacian u y = 0) {x : HCPolySupport.Vec d} (hx : x ∈ U) (i : Fin d) : 0 ≤ HCPolySupport.euclideanCoordLaplacian (fun (y : HCPolySupport.Vec d) => HCPolySupport.euclideanCoordDeriv i u y ^ 2) x

The squared coordinate derivative of a smooth harmonic function is subharmonic.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalized_radialIntegral_mono {d : ℕ} [NeZero d] {F : ℝ → ℝ} (hF : Continuous F) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hFmono : MonotoneOn F (Set.Ioc 0 b)) : ↑d / a ^ d * ∫ (t : ℝ) in 0..a, t ^ (d - 1) * F t ≤ ↑d / b ^ d * ∫ (t : ℝ) in 0..b, t ^ (d - 1) * F t

Pure one-dimensional radial arithmetic: the normalized weighted integral of a continuous nonnegative nondecreasing profile is nondecreasing.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integral_metricBall_eq_sphereMeasure_mul_radialSphereAverage {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : Continuous u) (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, u y = (Section4.Provider.ExcessDecay.Schauder.sphereMeasure d).real Set.univ * ∫ (s : ℝ) in 0..r, s ^ (d - 1) * Section4.Provider.ExcessDecay.Schauder.sphereAverage x s u

Polar decomposition of an integral over a Euclidean ball, normalized only at the sphere level.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_metricBall_toReal_eq_sphereMeasure_mul_pow_div {d : ℕ} [NeZero d] (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (Metric.ball x r)).toReal = (Section4.Provider.ExcessDecay.Schauder.sphereMeasure d).real Set.univ * (r ^ d / ↑d)

The real volume of a Euclidean ball, expressed with the surface measure normalization used by sphereAverage.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedIntegral_metricBall_eq_radialSphereAverage {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : Continuous u) (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (Metric.ball x r)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, u y = ↑d / r ^ d * ∫ (s : ℝ) in 0..r, s ^ (d - 1) * Section4.Provider.ExcessDecay.Schauder.sphereAverage x s u

Polar representation of the volume-normalized average on a Euclidean ball. The sphere-area constant cancels exactly.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedIntegral_metricBall_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) : (MeasureTheory.volume (Metric.ball x a)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball x a, u y ≤ (MeasureTheory.volume (Metric.ball x b)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball x b, u y

The volume-normalized ball average of a smooth subharmonic function is nondecreasing with the radius. This is the constant-one submean comparison needed by the Schauder iteration.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedIntegral_sq_euclideanCoordDeriv_mono {d : ℕ} [NeZero d] {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {z : HCPolySupport.Vec d} {R : ℝ} (hR : 0 < R) (hharm : ∀ y ∈ HCPolySupport.euclideanBall z R, HCPolySupport.euclideanCoordLaplacian u y = 0) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbR : b < R) (i : Fin d) : (MeasureTheory.volume (Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) a)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) a, HCPolySupport.euclideanCoordDeriv i u (Section4.Provider.ExcessDecay.Schauder.toEuc.symm y) ^ 2 ≤ (MeasureTheory.volume (Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) b)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) b, HCPolySupport.euclideanCoordDeriv i u (Section4.Provider.ExcessDecay.Schauder.toEuc.symm y) ^ 2

Constant-one normalized ball comparison for one squared coordinate of the gradient of a smooth coordinate-harmonic function.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedIntegral_vecNormSq_euclideanGradient_mono {d : ℕ} [NeZero d] {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {z : HCPolySupport.Vec d} {R : ℝ} (hR : 0 < R) (hharm : ∀ y ∈ HCPolySupport.euclideanBall z R, HCPolySupport.euclideanCoordLaplacian u y = 0) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbR : b < R) : (MeasureTheory.volume (Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) a)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) a, HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient u (Section4.Provider.ExcessDecay.Schauder.toEuc.symm y)) ≤ (MeasureTheory.volume (Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) b)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) b, HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient u (Section4.Provider.ExcessDecay.Schauder.toEuc.symm y))

The smooth constant-one comparison after summing all gradient coordinates.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volumeAverage_vecNormSq_euclideanGradient_euclideanBall_eq {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : (HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z r) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient v x)) = (MeasureTheory.volume (Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) r)).toReal⁻¹ * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball (Section4.Provider.ExcessDecay.Schauder.toEuc z) r, HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient v (Section4.Provider.ExcessDecay.Schauder.toEuc.symm y))

The measure-preserving coordinate dictionary for normalized smooth gradient energy on a Euclidean ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volumeAverage_vecNormSq_euclideanGradient_mono {d : ℕ} [NeZero d] {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {z : HCPolySupport.Vec d} {R : ℝ} (hR : 0 < R) (hharm : ∀ y ∈ HCPolySupport.euclideanBall z R, HCPolySupport.euclideanCoordLaplacian u y = 0) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbR : b < R) : (HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z a) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient u x)) ≤ HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z b) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (HCPolySupport.euclideanGradient u x)

Constant-one normalized energy comparison for a globally smooth coordinate-harmonic function.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volumeAverage_vecNormSq_grad_mono_euclideanBall_lt {d : ℕ} [NeZero d] {z : HCPolySupport.Vec d} {R : ℝ} (hR : 0 < R) (h : HCPolySupport.H1Function (HCPolySupport.euclideanBall z R)) (hh : IsUnitWeaklyHarmonicOn (HCPolySupport.euclideanBall z R) h) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbR : b < R) : (HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z a) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (h.grad x)) ≤ HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z b) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (h.grad x)

Constant-one comparison for the weak gradient, with the outer comparison radius strictly inside the weak-harmonicity ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_euclideanBall_toReal_eq_sphereMeasure_mul_pow_div {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal = (Section4.Provider.ExcessDecay.Schauder.sphereMeasure d).real Set.univ * (r ^ d / ↑d)

Exact real volume of the project-carrier Euclidean ball, in the same surface-area normalization as the polar formula.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volumeAverage_vecNormSq_grad_mono_euclideanBall {d : ℕ} [NeZero d] {z : HCPolySupport.Vec d} {R s : ℝ} (hR : 0 < R) (hs : 0 < s) (hsR : s ≤ R) (h : HCPolySupport.H1Function (HCPolySupport.euclideanBall z R)) (hh : IsUnitWeaklyHarmonicOn (HCPolySupport.euclideanBall z R) h) : (HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z s) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (h.grad x)) ≤ HCPolySupport.volumeAverage (HCPolySupport.euclideanBall z R) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (h.grad x)

The weak-gradient normalized energy comparison including the outer radius. The endpoint is obtained from the strict comparison and exact ball volume continuity; no interior-estimate constant is spent.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_grad_mono_euclideanBall {d : ℕ} [NeZero d] {z : HCPolySupport.Vec d} {R s : ℝ} (hR : 0 < R) (hs : 0 < s) (hsR : s ≤ R) (h : HCPolySupport.H1Function (HCPolySupport.euclideanBall z R)) (hh : IsUnitWeaklyHarmonicOn (HCPolySupport.euclideanBall z R) h) : vectorNormalizedL2On (HCPolySupport.euclideanBall z s) h.grad ≤ vectorNormalizedL2On (HCPolySupport.euclideanBall z R) h.grad

The manuscript-facing constant-one concentric-ball comparison for the normalized L² norm of the weak harmonic gradient.