OneStepSchauderPolar

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

Polar decomposition and continuity of the spherical flux

Two ingredients of the flux-vanishing crux behind the mean value property:

• the polar bridge — a ball integral against Lebesgue measure written as an iterated radius/sphere integral, which is what turns the flux identity into an identity about a one-variable function of the radius;
• continuity of the spherical flux in the radius, needed before the fundamental theorem of calculus can be applied to it.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_eq_integral_Ioi_sphere {d : ℕ} [NeZero d] {G : EuclideanSpace ℝ (Fin d) → ℝ} (hG : MeasureTheory.Integrable G MeasureTheory.volume) : ∫ (z : EuclideanSpace ℝ (Fin d)), G z = ∫ (r : ℝ) in Set.Ioi 0, r ^ (d - 1) • ∫ (ω : ↑(Metric.sphere 0 1)), G (r • ↑ω) ∂sphereMeasure d

The general polar-coordinate bridge. For an integrable scalar function G on EuclideanSpace ℝ (Fin d) (d ≥ 1), ∫ z, G z = ∫ r in (0, ∞), r ^ (d - 1) • (∫ ω, G (r • ω) dσ(ω)),

the disintegration of Lebesgue measure into the surface measure sphereMeasure d on the unit sphere and the radial density r ^ (d - 1) dr.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuousAt_sphereFlux {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 1 u) (x : EuclideanSpace ℝ (Fin d)) (r₀ : ℝ) : ContinuousAt (fun (r : ℝ) => sphereFlux x r u) r₀

Continuity of the radial flux (at a point). For C¹ u, the average radial flux r ↦ sphereFlux x r u is continuous at every r₀.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuous_sphereFlux {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 1 u) (x : EuclideanSpace ℝ (Fin d)) : Continuous fun (r : ℝ) => sphereFlux x r u

Continuity of the radial flux. For C¹ u, the average radial flux is continuous in r.