OneStepSchauderInteriorGrad

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

Differentiating the reproducing convolution; the L²/L¹ bookkeeping

• The pointwise gradient half. Differentiating the reproducing convolution once moves the derivative onto the kernel: ∇w(x₀) = ((∇K_ε) ⋆ w)(x₀), hence ‖∇w(x₀)‖ ≤ ‖∇K_ε‖_∞ · ∫_{B(x₀,2ε)} |w|.
• The L² half. The Cauchy–Schwarz upgrade (∫_s |f|)² ≤ |s| · ∫_s f² (sq_setIntegral_abs_le) and the measure-preserving transfer of the CoarseGraining meanSquareDeviationOn on euclideanBall to the volume-normalized L² deviation on the Mathlib metric ball (meanSquareDeviationOn_euclideanBall_eq).

Constant-subtraction stays harmonic

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_const {d : ℕ} (c : ℝ) (s : Set (EuclideanSpace ℝ (Fin d))) : InnerProductSpace.HarmonicOnNhd (fun (x : EuclideanSpace ℝ (Fin d)) => c) s

A constant function is harmonic in a neighbourhood of any set.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_sub_const {d : ℕ} {v : EuclideanSpace ℝ (Fin d) → ℝ} {s : Set (EuclideanSpace ℝ (Fin d))} (hv : InnerProductSpace.HarmonicOnNhd v s) (c : ℝ) : InnerProductSpace.HarmonicOnNhd (fun (y : EuclideanSpace ℝ (Fin d)) => v y - c) s

A harmonic function minus a constant is harmonic.

The core estimate

The interior gradient bound

A sup bound for the unit-kernel gradient

The core L¹ gradient bound

Cauchy–Schwarz on the ball

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sq_setIntegral_abs_le {d : ℕ} (s : Set (EuclideanSpace ℝ (Fin d))) (hs : MeasurableSet s) (hμ : MeasureTheory.volume s ≠ ⊤) {f : EuclideanSpace ℝ (Fin d) → ℝ} {Mf : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict s)) (hfb : ∀ᵐ (y : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict s, |f y| ≤ Mf) : (∫ (y : EuclideanSpace ℝ (Fin d)) in s, |f y|) ^ 2 ≤ (MeasureTheory.volume s).toReal * ∫ (y : EuclideanSpace ℝ (Fin d)) in s, f y ^ 2

Cauchy–Schwarz on a finite-measure set. (∫_s |f|)² ≤ vol(s) · ∫_s f² for f a.e.-bounded on s. Applied with s a ball and f = w.

The measure-preserving coordinate transfer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.measurePreserving_toEuc (d : ℕ) : MeasureTheory.MeasurePreserving (⇑toEuc) MeasureTheory.volume MeasureTheory.volume

toEuc = toLp 2 is volume preserving (it is the identity on underlying data).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.measurableEmbedding_toEuc (d : ℕ) : MeasurableEmbedding ⇑toEuc

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.preimage_ball_toEuc {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : ⇑toEuc ⁻¹' Metric.ball x r = HCPolySupport.euclideanBall (toEuc.symm x) r

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.meanSquareDeviationOn_euclideanBall_eq {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) (c : ℝ) : HCPolySupport.Book.Ch01.meanSquareDeviationOn (HCPolySupport.euclideanBall (toEuc.symm x) r) (u ∘ ⇑toEuc) c = (MeasureTheory.volume (Metric.ball x r)).toReal⁻¹ * ∫ (z : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, (u z - c) ^ 2

Transfer of the mean-square deviation. The CoarseGraining volume-averaged mean-square deviation on the explicit euclideanBall, of u ∘ toEuc, equals the volume-normalized L² deviation of u on the mathlib metric ball, via the measure-preserving identification toEuc.

The interior gradient estimate, L²-deviation shape (native)