OneStepSchauderBridge

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

The coordinate identification Vec d ≃L EuclideanSpace ℝ (Fin d)

The interior Schauder estimate for the harmonic competitor of the Schauder gradient-Hölder estimate is proved against Mathlib's InnerProductSpace.HarmonicOnNhd, which lives on EuclideanSpace ℝ (Fin d) with Metric.ball and the coordinate-free Laplacian Δ. Every §4 carrier (Vec d, truncatedWindow, HolderSeminormBoundOn, affineExcess) lives on the CoarseGraining coordinate carrier Vec d = Fin d → ℝ with the sup norm.

This module is the definitional dictionary between the two, through the canonical identification toEuc : Vec d ≃L[ℝ] EuclideanSpace ℝ (Fin d) (the identity on underlying data; only the ambient norm differs):

• toEuc, toEuc_apply, toEuc_basisVec;
• mem_euclideanBall_toEuc_iff — the ball dictionary toEuc a ∈ Metric.ball (toEuc b) r ↔ a ∈ euclideanBall b r;
• norm_toEuc_le, norm_le_norm_toEuc — the two-sided comparison of the sup and ℓ² norms with the sharp constants √d and 1, the source of every dimensional factor in the Schauder constant;
• norm_fderiv_vec_sub_le — the resulting transfer of gradient Hölder differences;
• harmonicOnNhd_sub_vec_affine — subtracting a Vec d affine competitor preserves harmonicity of the Euclidean avatar. This is what turns a constant-deviation interior estimate into a genuine excess estimate.

1. The coordinate identification

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc {d : ℕ} : HCPolySupport.Vec d ≃L[ℝ] EuclideanSpace ℝ (Fin d)

The canonical identification of the CoarseGraining coordinate carrier Vec d = Fin d → ℝ with the Mathlib inner-product space EuclideanSpace ℝ (Fin d). It is the identity on underlying data; only the ambient norm (sup vs. ℓ²) differs.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc = (EuclideanSpace.equiv (Fin d) ℝ).symm

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_apply {d : ℕ} (y : HCPolySupport.Vec d) (i : Fin d) : (toEuc y).ofLp i = y i

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_symm_apply {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (i : Fin d) : toEuc.symm x i = x.ofLp i

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_basisVec {d : ℕ} (i : Fin d) : toEuc (HCPolySupport.basisVec i) = EuclideanSpace.single i 1

The coordinate basis vector basisVec i maps to the orthonormal basis vector EuclideanSpace.single i 1.

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_symm_single {d : ℕ} (i : Fin d) : toEuc.symm (EuclideanSpace.single i 1) = HCPolySupport.basisVec i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.comp_toEuc_symm_toEuc {d : ℕ} (v : HCPolySupport.Vec d → ℝ) : (v ∘ ⇑toEuc.symm) ∘ ⇑toEuc = v

The round trip: a function on the Vec d carrier, pushed to the Euclidean carrier and pulled back, is itself.

2. The ball dictionary

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_sq_toEuc_sub {d : ℕ} (a b : HCPolySupport.Vec d) : ‖toEuc a - toEuc b‖ ^ 2 = HCPolySupport.euclideanSqDist a b

The ℓ² distance of two coordinate vectors, transported to EuclideanSpace, is the CoarseGraining Euclidean squared distance.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.mem_euclideanBall_toEuc_iff {d : ℕ} (a b : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : toEuc a ∈ Metric.ball (toEuc b) r ↔ a ∈ HCPolySupport.euclideanBall b r

Ball dictionary. Under the coordinate identification the Mathlib metric ball corresponds to the CoarseGraining explicit Euclidean ball.

3. The two-sided norm comparison

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_toEuc_le {d : ℕ} (y : HCPolySupport.Vec d) : ‖toEuc y‖ ≤ √↑d * ‖y‖

The ℓ² norm of a coordinate vector is at most √d times its sup norm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_le_norm_toEuc {d : ℕ} (y : HCPolySupport.Vec d) : ‖y‖ ≤ ‖toEuc y‖

The sup norm of a coordinate vector is at most its ℓ² norm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.opNorm_toEuc_le {d : ℕ} : ‖↑toEuc‖ ≤ √↑d

The operator norm of the coordinate identification, viewed as a continuous linear map from the sup-normed carrier to the ℓ²-normed one, is at most √d.

4. fderiv transfer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.fderiv_comp_toEuc {d : ℕ} (V : EuclideanSpace ℝ (Fin d) → ℝ) (y : HCPolySupport.Vec d) : fderiv ℝ (V ∘ ⇑toEuc) y = fderiv ℝ V (toEuc y) ∘SL ↑toEuc

Chain rule across the coordinate identification. No differentiability hypothesis is needed: if V is not differentiable at toEuc y then neither side is, and both are 0.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_fderiv_comp_toEuc_sub_le {d : ℕ} (V : EuclideanSpace ℝ (Fin d) → ℝ) (y z : HCPolySupport.Vec d) : ‖fderiv ℝ (V ∘ ⇑toEuc) y - fderiv ℝ (V ∘ ⇑toEuc) z‖ ≤ √↑d * ‖fderiv ℝ V (toEuc y) - fderiv ℝ V (toEuc z)‖

Hölder/Lipschitz seminorm transfer for fderiv. Differences of the derivative of V ∘ toEuc at the Vec d carrier are bounded by √d times the corresponding differences of fderiv V at the Euclidean carrier.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_fderiv_vec_sub_le {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (y z : HCPolySupport.Vec d) : ‖fderiv ℝ v y - fderiv ℝ v z‖ ≤ √↑d * ‖fderiv ℝ (v ∘ ⇑toEuc.symm) (toEuc y) - fderiv ℝ (v ∘ ⇑toEuc.symm) (toEuc z)‖

Hölder/Lipschitz seminorm transfer, Vec d shape.

5. Affine functions are harmonic

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.iteratedFDeriv_two_affine {d : ℕ} (c : ℝ) (L : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (x : EuclideanSpace ℝ (Fin d)) : iteratedFDeriv ℝ 2 (fun (z : EuclideanSpace ℝ (Fin d)) => c + L z) x = 0

The second iterated derivative of an affine function vanishes.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_affine {d : ℕ} (c : ℝ) (L : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : (Laplacian.laplacian fun (z : EuclideanSpace ℝ (Fin d)) => c + L z) = 0

The Laplacian of an affine function vanishes identically.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_affine {d : ℕ} (c : ℝ) (L : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (s : Set (EuclideanSpace ℝ (Fin d))) : InnerProductSpace.HarmonicOnNhd (fun (x : EuclideanSpace ℝ (Fin d)) => c + L x) s

Affine functions are harmonic. (Mathlib has no such lemma.)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_sub_affine {d : ℕ} {V : EuclideanSpace ℝ (Fin d) → ℝ} {s : Set (EuclideanSpace ℝ (Fin d))} (hV : InnerProductSpace.HarmonicOnNhd V s) (c : ℝ) (L : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : InnerProductSpace.HarmonicOnNhd (fun (x : EuclideanSpace ℝ (Fin d)) => V x - (c + L x)) s

Subtracting an affine competitor preserves harmonicity.

6. The Vec d affine competitor as a Euclidean continuous linear map

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

The CoarseGraining coordinate dot product vecDot g realized as a continuous linear functional on EuclideanSpace ℝ (Fin d): the inner product against toEuc g.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dotCLM g = (innerSL ℝ) (Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc g)

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dotCLM_apply {d : ℕ} (g : HCPolySupport.Vec d) (x : EuclideanSpace ℝ (Fin d)) : (dotCLM g) x = HCPolySupport.vecDot g (toEuc.symm x)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_sub_vec_affine {d : ℕ} {v : HCPolySupport.Vec d → ℝ} {s : Set (EuclideanSpace ℝ (Fin d))} (hv : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) s) (c : ℝ) (g : HCPolySupport.Vec d) : InnerProductSpace.HarmonicOnNhd ((fun (y : HCPolySupport.Vec d) => v y - (c + HCPolySupport.vecDot g y)) ∘ ⇑toEuc.symm) s

Subtracting a Vec d affine competitor preserves harmonicity. If the Euclidean avatar of v : Vec d → ℝ is harmonic, so is the avatar of y ↦ v y - (c + vecDot g y). This is the step that upgrades a constant-deviation interior estimate to an excess estimate.