OneStepSchauderExcess

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

The interior Schauder atom in the §4 excess vocabulary

OneStepSchauderInteriorHess bounds the Lipschitz seminorm of ∇u on the half-radius ball by C(d) r⁻² times the L² deviation of u from one constant, at the Euclidean carrier. Three moves turn that into the atom [∇v]_{Lip(B_{r/2})} ≤ C(d) r⁻² E_raw(v, B_r) the §4 excess machinery needs:

1. affine competitors. v − ℓ is harmonic for every affine ℓ (Schauder.harmonicOnNhd_sub_vec_affine), and ∇(v−ℓ)(y) − ∇(v−ℓ)(z) = ∇v(y) − ∇v(z). So the estimate holds against every competitor and passes to the infimum by le_mul_affineExcessRaw_of_forall — a constant-deviation bound becomes a genuine excess bound.
2. carrier transfer. Schauder.norm_fderiv_vec_sub_le and Schauder.norm_toEuc_le move the estimate from EuclideanSpace ℝ (Fin d) (ℓ² norm) to Vec d (sup norm) at the cost of √d · √d = d.
3. gradient field. HasGradientOn/HolderSeminormBoundOn of AffineSplitLift/Support are phrased through a gradient field G : Vec d → Vec d; gradField v y i := (fderiv ℝ v y) (basisVec i) is that field, slopeCLM_gradField identifies slope (gradField v y) with fderiv ℝ v y, and norm_gradField_sub_le bounds the sup-norm difference of the field by the operator-norm difference of the derivatives.

The excess carrier

The §4 excess carrier is Support.affineExcessRaw W v = sInf {‖v − ℓ‖_{L²(W)}} with Support.affineDistOn W v c g = Support.normalizedL2On W (v − affineEval c g).

1. Taking the infimum over affine competitors

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.le_mul_affineExcessRaw_of_forall {d : ℕ} {W : Set (HCPolySupport.Vec d)} {v : HCPolySupport.Vec d → ℝ} {A K : ℝ} (hK : 0 ≤ K) (h : ∀ (c : ℝ) (g : HCPolySupport.Vec d), A ≤ K * Support.affineDistOn W v c g) : A ≤ K * Support.affineExcessRaw W v

The infimum-taking step. If a quantity A is bounded by K times the L²(W) distance of v to every affine competitor (c, g), then it is bounded by K times the excess minimum affineExcessRaw W v.

This is the bridge from the harmonic interior estimates — which bound derivatives of v by the deviation of v from a fixed competitor, and which apply to v − ℓ for every affine ℓ because affine functions are harmonic — to the excess the §4 contraction is stated in.

2. The dimensional constant

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.schauderConst (d : ℕ) [NeZero d] : ℝ

The dimensional constant of the interior Schauder atom: d times the constant of the native interior gradient-Lipschitz estimate interiorGradLipschitz_le_l2dev. The factor d is the round-trip cost √d · √d of the Vec d ↔ EuclideanSpace ℝ (Fin d) norm comparison.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.schauderConst d = ↑d * ⋯.choose

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.schauderConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ schauderConst d

3. Differentiability and the affine competitor at the Vec d carrier

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.differentiableAt_of_harmonic_avatar {d : ℕ} {v : HCPolySupport.Vec d → ℝ} {s : Set (EuclideanSpace ℝ (Fin d))} (hv : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) s) {y : HCPolySupport.Vec d} (hy : toEuc y ∈ s) : DifferentiableAt ℝ v y

Differentiability at the Vec d carrier from harmonicity of the Euclidean avatar.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.vecDotCLM {d : ℕ} (g : HCPolySupport.Vec d) : HCPolySupport.Vec d →L[ℝ] ℝ

The Vec d affine slope x ↦ g · x as a continuous linear functional.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.vecDotCLM g = Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dotCLM g ∘SL ↑Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.vecDotCLM_apply {d : ℕ} (g x : HCPolySupport.Vec d) : (vecDotCLM g) x = HCPolySupport.vecDot g x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hasFDerivAt_affineEval {d : ℕ} (c : ℝ) (g y : HCPolySupport.Vec d) : HasFDerivAt (Support.affineEval c g) (vecDotCLM g) y

The affine function affineEval c g has derivative vecDot g everywhere.

4. The interior Schauder atom in the excess vocabulary

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradLipschitz_le_affineExcessRaw_of_harmonic {d : ℕ} [NeZero d] {v : HCPolySupport.Vec d → ℝ} {a : HCPolySupport.Vec d} {r R : ℝ} (hr : 0 < r) (hR : r < R) (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) (Metric.ball (toEuc a) R)) {y z : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.euclideanBall a (r / 2)) (hz : z ∈ HCPolySupport.euclideanBall a (r / 2)) : ‖fderiv ℝ v y - fderiv ℝ v z‖ ≤ schauderConst d * r⁻¹ * r⁻¹ * Support.affineExcessRaw (HCPolySupport.euclideanBall a r) v * ‖y - z‖

The interior Schauder atom, Vec d carrier. For v whose Euclidean avatar is harmonic on B(toEuc a, R) and any 0 < r < R, the gradient of v is Lipschitz on euclideanBall a (r/2) with constant

schauderConst d · r⁻¹ · r⁻¹ · affineExcessRaw (euclideanBall a r) v.

5. The gradient field

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradField {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (y : HCPolySupport.Vec d) : HCPolySupport.Vec d

The gradient field of v in the Vec d carrier: the coordinate values of fderiv ℝ v.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradField v y i = (fderiv ℝ v y) (HCPolySupport.basisVec i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradField_apply {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (y : HCPolySupport.Vec d) (i : Fin d) : gradField v y i = (fderiv ℝ v y) (HCPolySupport.basisVec i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sum_smul_basisVec {d : ℕ} (w : HCPolySupport.Vec d) : ∑ i : Fin d, w i • HCPolySupport.basisVec i = w

A coordinate vector is the sum of its coordinates against the basis.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.slopeCLM_gradField {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (y : HCPolySupport.Vec d) : Support.slopeCLM (gradField v y) = fderiv ℝ v y

The gradient field realizes the derivative. slope (gradField v y) is fderiv ℝ v y.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_basisVec_eq_one {d : ℕ} (i : Fin d) : ‖HCPolySupport.basisVec i‖ = 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_gradField_sub_le {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (x y : HCPolySupport.Vec d) : ‖gradField v x - gradField v y‖ ≤ ‖fderiv ℝ v x - fderiv ℝ v y‖

From operator norms to gradient-field sup norms. The sup norm of the difference of the gradient fields is at most the operator norm of the difference of the derivatives.