OneStepSchauderInterior

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

The ball → window transfer of the interior Schauder atom

OneStepSchauderExcess.gradLipschitz_le_affineExcessRaw_of_harmonic gives the gradient-Lipschitz bound for y, z inside one Euclidean ball euclideanBall a (r/2) on which the harmonic function is controlled. The §4 consumer needs the bound on a window — a truncated triadic cube — which is not contained in any such ball at the available margin: the sup ↔ ℓ² loss is √d, while only one triadic scale (a factor 3) separates the Hölder window from the harmonicity domain, so for d ≥ 3 no single admissible ball covers the window. (This is a genuine structural point, not a bookkeeping one: the bound being propagated is a bound on differences of ∇v, and ∇v itself is not controlled by the excess — adding a linear function changes ∇v by a constant and leaves the excess fixed — so the "far pairs" of the window cannot be handled by a sup bound. They must be handled by chaining.)

This module supplies the two missing moves.

• norm_sub_le_of_local_bound — local-to-global on a convex set. A bound ‖G p − G q‖ ≤ L ‖p − q‖ valid only for pairs at sup-distance < ρ upgrades, on a convex set, to the same bound for all pairs: subdivide the segment [p,q] (which stays in the set) into N steps of length < ρ and telescope. The constant is unchanged, and no sign hypothesis on it is needed.
• affineExcessRaw_le_of_subset_mul — the volume-ratio comparison of the excess minimum on nested windows, E_raw(W', v) ≤ (|W|/|W'|)^{1/2} E_raw(W, v), obtained competitor-by-competitor from Support.normalizedL2On_le_of_subset and passed to the two infima by le_mul_affineExcessRaw_of_forall.

Combining them with the atom gives gradField_lipschitzOn_of_harmonic: a gradient-Lipschitz bound for gradField v on the whole convex window W, against the excess on the enveloping window W₂. holderHalf_of_lipschitzOn then weakens α = 1 to the printed α = 1/2 at the cost of √(diam W) (Hölder monotonicity on a bounded set).

1. Local-to-global on a convex set

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_sub_le_of_local_bound {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW : Convex ℝ W) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {L rho : ℝ} (hrho : 0 < rho) (hloc : ∀ p ∈ W, ∀ q ∈ W, ‖p - q‖ < rho → ‖G p - G q‖ ≤ L * ‖p - q‖) {y z : HCPolySupport.Vec d} (hy : y ∈ W) (hz : z ∈ W) : ‖G y - G z‖ ≤ L * ‖y - z‖

Local-to-global on a convex set. A bound on ‖G p − G q‖ proportional to ‖p − q‖, valid only for pairs at sup-distance < ρ, holds for all pairs of a convex set, with the same constant. The segment [p,q] is subdivided into N steps shorter than ρ and the estimate telescopes.

2. The volume-ratio comparison of the excess minimum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineExcessRaw_le_of_subset_mul {d : ℕ} {W W' : Set (HCPolySupport.Vec d)} {v : HCPolySupport.Vec d → ℝ} (hsub : W' ⊆ W) (hW : 0 < (MeasureTheory.volume W).toReal) (hW' : 0 < (MeasureTheory.volume W').toReal) (hint : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (v x - Support.affineEval c g x) ^ 2) W MeasureTheory.volume) : Support.affineExcessRaw W' v ≤ √((MeasureTheory.volume W).toReal / (MeasureTheory.volume W').toReal) * Support.affineExcessRaw W v

Window comparison for the excess minimum. For W' ⊆ W of positive finite volume, E_raw(v, W') ≤ (|W|/|W'|)^{1/2} · E_raw(v, W). Competitor by competitor this is Support.normalizedL2On_le_of_subset; the passage to the two infima is le_mul_affineExcessRaw_of_forall.

3. Hölder monotonicity α = 1 → α = 1/2

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.holderHalf_of_lipschitzOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {L D : ℝ} (hL : 0 ≤ L) (hlip : ∀ p ∈ U, ∀ q ∈ U, ‖G p - G q‖ ≤ L * ‖p - q‖) (hdiam : ∀ p ∈ U, ∀ q ∈ U, ‖p - q‖ ≤ D) : Support.HolderSeminormBoundOn U (1 / 2) (L * √D) G

α = 1 → α = 1/2 on a bounded set. A Lipschitz bound with constant L on a set of sup-diameter at most D is a C^{0,1/2} bound with constant L √D.

4. Ball geometry at the Vec d carrier

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanSqDist_self {d : ℕ} (p : HCPolySupport.Vec d) : HCPolySupport.euclideanSqDist p p = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.mem_euclideanBall_self {d : ℕ} {p : HCPolySupport.Vec d} {rho : ℝ} (h : 0 < rho) : p ∈ HCPolySupport.euclideanBall p rho

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.mem_euclideanBall_of_norm_lt {d : ℕ} {p q : HCPolySupport.Vec d} {rho : ℝ} (h : √↑d * ‖q - p‖ < rho) : q ∈ HCPolySupport.euclideanBall p rho

The sup-norm ball of radius s sits inside the Euclidean ball of radius √d · s: the two-sided norm comparison, in ball form.

5. The gradient-Lipschitz bound on a convex window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradField_lipschitzOn_of_harmonic {d : ℕ} [NeZero d] {S : Set (EuclideanSpace ℝ (Fin d))} {v : HCPolySupport.Vec d → ℝ} {W W₂ : Set (HCPolySupport.Vec d)} {R ratio : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) S) (hWconv : Convex ℝ W) (hR : 0 < R) (hratio0 : 0 ≤ ratio) (hballS : ∀ p ∈ W, Metric.ball (toEuc p) R ⊆ S) (hsub : ∀ p ∈ W, HCPolySupport.euclideanBall p (R / 2) ⊆ W₂) (hW₂ : 0 < (MeasureTheory.volume W₂).toReal) (hballvol : ∀ p ∈ W, 0 < (MeasureTheory.volume (HCPolySupport.euclideanBall p (R / 2))).toReal) (hratio : ∀ p ∈ W, √((MeasureTheory.volume W₂).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall p (R / 2))).toReal) ≤ ratio) (hint : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (v x - Support.affineEval c g x) ^ 2) W₂ MeasureTheory.volume) (p : HCPolySupport.Vec d) : p ∈ W → ∀ q ∈ W, ‖gradField v p - gradField v q‖ ≤ 4 * schauderConst d * R⁻¹ * R⁻¹ * (ratio * Support.affineExcessRaw W₂ v) * ‖p - q‖

The interior Schauder atom on a convex window.

Hypotheses, in words: v's Euclidean avatar is harmonic on S; W is a convex window each of whose points p carries an admissible ball Metric.ball (toEuc p) R ⊆ S; the half-balls euclideanBall p (R/2) all sit inside an enveloping window W₂ whose volume ratio against them is at most ratio². Conclusion: gradField v is Lipschitz on all of W with constant

4 · schauderConst d · R⁻¹ · R⁻¹ · ratio · E_raw(W₂, v).

The factor 4 is (R/2)⁻¹(R/2)⁻¹ / (R⁻¹R⁻¹); the factor ratio is the window transfer; E_raw is the §4 excess minimum on W₂.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.gradField_holderHalf_of_harmonic {d : ℕ} [NeZero d] {S : Set (EuclideanSpace ℝ (Fin d))} {v : HCPolySupport.Vec d → ℝ} {W W₂ : Set (HCPolySupport.Vec d)} {R ratio D : ℝ} (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) S) (hWconv : Convex ℝ W) (hR : 0 < R) (hratio0 : 0 ≤ ratio) (hballS : ∀ p ∈ W, Metric.ball (toEuc p) R ⊆ S) (hsub : ∀ p ∈ W, HCPolySupport.euclideanBall p (R / 2) ⊆ W₂) (hW₂ : 0 < (MeasureTheory.volume W₂).toReal) (hballvol : ∀ p ∈ W, 0 < (MeasureTheory.volume (HCPolySupport.euclideanBall p (R / 2))).toReal) (hratio : ∀ p ∈ W, √((MeasureTheory.volume W₂).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall p (R / 2))).toReal) ≤ ratio) (hint : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (v x - Support.affineEval c g x) ^ 2) W₂ MeasureTheory.volume) (hdiam : ∀ p ∈ W, ∀ q ∈ W, ‖p - q‖ ≤ D) : Support.HolderSeminormBoundOn W (1 / 2) (4 * schauderConst d * R⁻¹ * R⁻¹ * (ratio * Support.affineExcessRaw W₂ v) * √D) (gradField v)

The interior Schauder atom, C^{0,1/2} form on a convex window.