OneStepSchauderSphere

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

Sphere averages and the mean value property

The reproducing-convolution route of the Schauder gradient-Hölder estimate rests on the mean value property of harmonic functions. This module builds it:

• sphereAverage f x r — the average of f over the sphere of radius r around x, realized as an integral over the unit sphere so that the radius is a smooth parameter;
• hasDerivAt_sphereAverage — differentiation under the integral sign in the radius;
• the mean value property itself: a function whose spherical flux vanishes has a radius-independent sphere average, hence equals its own sphere average.

The surface measure on the unit sphere

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereMeasure (d : ℕ) : MeasureTheory.Measure ↑(Metric.sphere 0 1)

The surface measure on the unit sphere of EuclideanSpace ℝ (Fin d): the mathlib push of the Lebesgue (additive Haar) volume onto Metric.sphere 0 1 via Measure.toSphere. For d ≥ 1 it is a finite, strictly positive measure, so it normalizes the spherical average.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereMeasure d = MeasureTheory.volume.toSphere

instance Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.instIsFiniteMeasureSphereMeasure {d : ℕ} : MeasureTheory.IsFiniteMeasure (sphereMeasure d)

instance Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.instNeZeroSphereMeasure {d : ℕ} [NeZero d] : NeZero (sphereMeasure d)

For d ≥ 1 the ambient space is nontrivial, hence the surface measure is nonzero.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereMeasure_univ_ne_zero {d : ℕ} [NeZero d] : (sphereMeasure d) Set.univ ≠ 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereMeasure_real_univ_ne_zero {d : ℕ} [NeZero d] : (sphereMeasure d).real Set.univ ≠ 0

The spherical average

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : ℝ

The normalized spherical average of u over ∂B(x, r), written as the average of the dilated-translated function ω ↦ u (x + r • ω) over the unit sphere. (Native port of K euclideanL2SphereAverage.)

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage x r u = ⨍ (ω : ↑(Metric.sphere 0 1)), u (x + r • ↑ω) ∂Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereMeasure d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_def {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : sphereAverage x r u = ⨍ (ω : ↑(Metric.sphere 0 1)), u (x + r • ↑ω) ∂sphereMeasure d

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_const {d : ℕ} [NeZero d] (x : EuclideanSpace ℝ (Fin d)) (r c : ℝ) : (sphereAverage x r fun (x : EuclideanSpace ℝ (Fin d)) => c) = c

The spherical average of a constant is that constant.

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_zero {d : ℕ} [NeZero d] (x : EuclideanSpace ℝ (Fin d)) (u : EuclideanSpace ℝ (Fin d) → ℝ) : sphereAverage x 0 u = u x

The spherical average at radius 0 is point evaluation at the center.

Continuity in the radius

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuousAt_sphereAverage {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (huc : Continuous u) (x : EuclideanSpace ℝ (Fin d)) (r₀ : ℝ) : ContinuousAt (fun (r : ℝ) => sphereAverage x r u) r₀

Continuity in the radius (at a point). For continuous u, the spherical average r ↦ sphereAverage x r u is continuous at every r₀. Proof: dominated convergence with the local bound obtained from continuity of u on the compact ball closedBall x (|r₀| + 1).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuous_sphereAverage {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (huc : Continuous u) (x : EuclideanSpace ℝ (Fin d)) : Continuous fun (r : ℝ) => sphereAverage x r u

Continuity in the radius. For continuous u, the spherical average is continuous in r.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hasDerivAt_sphereAverage {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 1 u) (x : EuclideanSpace ℝ (Fin d)) (r₀ : ℝ) : HasDerivAt (fun (r : ℝ) => sphereAverage x r u) (((sphereMeasure d).real Set.univ)⁻¹ • ∫ (ω : ↑(Metric.sphere 0 1)), (fderiv ℝ u (x + r₀ • ↑ω)) ↑ω ∂sphereMeasure d) r₀

Radial derivative of the spherical average. For a C¹ function u, the spherical average r ↦ sphereAverage x r u is differentiable at every r₀, with derivative the spherical average of the radial directional derivative ω ↦ ⟨∇u(x + r₀ ω), ω⟩.

This is proved by differentiation under the integral sign, with the local gradient bound coming from continuity of fderiv u on the compact ball closedBall x (|r₀| + 1). It is the half of the mean-value property that does not need the divergence theorem.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereFlux {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : ℝ

The average radial flux of ∇u over the unit sphere at radius r about x: ∫_S ⟨∇u(x + r ω), ω⟩ dσ(ω), written with fderiv. This is exactly the integral appearing in the radial derivative hasDerivAt_sphereAverage; its vanishing for harmonic u is the classical divergence-theorem input to the mean value property.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereFlux_def {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : sphereFlux x r u = ∫ (ω : ↑(Metric.sphere 0 1)), (fderiv ℝ u (x + r • ↑ω)) ↑ω ∂sphereMeasure d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_const_of_flux_zero {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 1 u) (x : EuclideanSpace ℝ (Fin d)) {R : ℝ} (hflux : ∀ r ∈ Set.Ioo 0 R, sphereFlux x r u = 0) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hb : b < R) : sphereAverage x a u = sphereAverage x b u

Sphere average is constant on (0, R) under flux vanishing. If u is C¹ and the average radial flux sphereFlux x r u vanishes for every r ∈ (0, R), then the spherical average is constant across that radius range: for 0 < a ≤ b < R, sphereAverage x a u = sphereAverage x b u.

The derivative of r ↦ sphereAverage x r u is ‖S‖⁻¹ • sphereFlux x r u (hasDerivAt_sphereAverage), so the hypothesis makes it vanish on (0, R); constant_of_has_deriv_right_zero on [a, b] concludes constancy.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sphereAverage_eq_center_of_flux_zero {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 1 u) (x : EuclideanSpace ℝ (Fin d)) {R : ℝ} (hflux : ∀ r ∈ Set.Ioo 0 R, sphereFlux x r u = 0) (r : ℝ) : r ∈ Set.Ico 0 R → sphereAverage x r u = u x

Spherical mean value property, modulo flux vanishing. If u is C¹ and the average radial flux vanishes on (0, R), then the spherical average equals the center value at every radius in [0, R): sphereAverage x r u = u x.

The extension of constancy from (0, R) down to the center r = 0 uses continuity of the average in the radius.