OneStepSchauderReproducing

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

The reproducing convolution

A harmonic function reproduces itself against any unit-mass radial kernel: integrating the mean value property in the radius against the radial profile gives u(x₀) = (K_ε ⋆ u)(x₀) whenever K_ε is supported in a ball on which u is harmonic. This module proves that identity and packages it as a convolution, which is the exact form the interior estimates differentiate.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.reproducing_of_radial {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) {K : EuclideanSpace ℝ (Fin d) → ℝ} (hKc : Continuous K) (hKcs : HasCompactSupport K) (hKrad : ∀ {a b : EuclideanSpace ℝ (Fin d)}, ‖a‖ = ‖b‖ → K a = K b) {ρ : ℝ} (hρR : ρ ≤ R) (hKsupp : ∀ (z : EuclideanSpace ℝ (Fin d)), ρ ≤ ‖z‖ → K z = 0) (hKmass : ∫ (z : EuclideanSpace ℝ (Fin d)), K z = 1) : ∫ (y : EuclideanSpace ℝ (Fin d)), K (y - x) * u y = u x

Reproducing identity for a radial kernel. Let u ∈ C² be harmonic on Metric.ball x R and let K be a continuous, radial, compactly supported kernel of unit mass whose support sits inside the ball of radius ρ ≤ R (i.e. K z = 0 whenever ρ ≤ ‖z‖). Then K reproduces u at the center: ∫ y, K (y - x) · u y = u x.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.convolution_radialKernelScaled_indicator_apply {d : ℕ} [NeZero d] {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) {x₀ x' : EuclideanSpace ℝ (Fin d)} {r₀ ε R' : ℝ} (hε : 0 < ε) (hεR' : ε ≤ R') (hball : Metric.ball x' ε ⊆ Metric.ball x₀ r₀) (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball x' R')) : MeasureTheory.convolution (radialKernelScaled d ε) ((Metric.ball x₀ r₀).indicator u) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x' = u x'

Pointwise value of the mollified reproducing convolution. Let u ∈ C² be harmonic on Metric.ball x' R' with ε ≤ R', and suppose the ε-ball around x' sits inside the localization ball ball x₀ r₀. Then the convolution of the ε-scaled kernel with the localized field evaluates to u x' at x'.