CubeSchauderOneStep

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

Cube Schauder: the interior one-step contraction at the Lipschitz rate

The proved ExcessDecay.excessDecay_oneStep_triangle_of_schauder contracts at C(d)·3^{-k/2}, which is the same rate as the forcing remainder: theta/rho = C(d) is k-independent and larger than 1, so no gap exists and the Campanato exponent tops out strictly below 1/2. That route cannot reach the frozen external's inclusive endpoint s ≤ 1/2.

This module re-derives the interior one step from the Lipschitz atom ExcessDecay.gradField_lipschitzOn_of_harmonic (α = 1, the pointwise C^{1,1} estimate for harmonic functions) instead of its C^{0,1/2} corollary, and the contraction factor improves to C(d)·3^{-k}:

  E(u, U_k) ≤ C_contr(d) · 3^{-k} · E(u, U_0)
              + C_rem(d,k) · 3^{-n} · ‖u - v‖_{L²(U_2)} ,

U_j = (x + □_{n-j}) ∩ □_m. Since the remainder decays at 3^{-k/2} per step (the freezing gain of a C^{0,1/2} forcing), theta = C_contr(d) 3^{-k} is strictly below rho = 3^{-k/2} as soon as C_contr(d) < 3^{k/2}, and the gap is then uniform. That is the resolution the development's rate question needed; CubeSchauderCampanato fixes the step size and runs the iteration.

Why the exponent improves

A first-order Taylor competitor built from a gradient which is only C^{0,1/2}(U) has residual K·r^{3/2} on a window of radius r, hence excess K·r^{1/2}; built from a Lipschitz gradient it has residual L·r², hence excess L·r. Feeding the harmonic gradient-Lipschitz bound L ≲ 3^{-n} E(v,U_2) gives E(v,U_k) ≲ 3^{-n}·3^{n-k}·E(v,U_2) = 3^{-k}E(v,U_2) — one full power of the scale instead of a half.

Main results

• abs_sub_affineLift_volumeAverage_le_lipschitz — the mean-value residual 2 d L r² at a Lipschitz gradient field.
• affineExcess_le_taylorLipschitz — E(f,W) ≤ (9d/2) · L · 3^k on the truncated window of scale k.
• exists_gradientLipschitz_interior — the harmonic gradient-Lipschitz bound in the window vocabulary, at a constant multiple of 3^{-n} · E(v,U_2).
• excessDecay_oneStep_lipschitz — the displayed one-step contraction.

References

• Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), Proposition p.Schauder.C1alpha, display e.Sch1a.1.
• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. The mean-value residual at a Lipschitz gradient

theorem Algsuperdiff.Section4.Provider.Schauder.abs_sub_affineLift_volumeAverage_le_lipschitz {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {L r : ℝ} {x y : HCPolySupport.Vec d} (hW : Convex ℝ W) (hx : x ∈ W) (hy : y ∈ W) (hL : 0 ≤ L) (hr0 : 0 ≤ r) (hvolpos : 0 < MeasureTheory.volume W) (hvoltop : MeasureTheory.volume W < ⊤) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) W MeasureTheory.volume) (hf : Support.HasGradientOn W f G) (hG : ∀ p ∈ W, ∀ q ∈ W, ‖G p - G q‖ ≤ L * ‖p - q‖) (hdiam : ∀ p ∈ W, ‖p - x‖ ≤ r) : |f y - ExcessDecay.affineLift x (f x) (HCPolySupport.volumeAverageVec W G) y| ≤ 2 * ↑d * L * r ^ 2

The affine-lift residual, Lipschitz gradient.

If f has gradient field G on the convex window W of sup-radius r around x, and G is L-Lipschitz on W, then f differs from its affine lift at x (built with the average gradient) by at most 2 d L r².

This is the α = 1 sibling of ExcessDecay.abs_sub_affineLift_volumeAverage_le, whose α = 1/2 hypothesis yields the weaker 2 d K r^{3/2}.

2. The Lipschitz affine competitor on a truncated window

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcessRaw_le_taylorLipschitz {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {L : ℝ} (hL : 0 ≤ L) (hmem : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m k))) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (ExcessDecay.truncatedWindow x m k) MeasureTheory.volume) (hf : Support.HasGradientOn (ExcessDecay.truncatedWindow x m k) f G) (hG : ∀ p ∈ ExcessDecay.truncatedWindow x m k, ∀ q ∈ ExcessDecay.truncatedWindow x m k, ‖G p - G q‖ ≤ L * ‖p - q‖) : Support.affineExcessRaw (ExcessDecay.truncatedWindow x m k) f ≤ 2 * ↑d * L * (3 ^ k / 2) ^ 2

The raw Lipschitz Taylor bound on the truncated window of scale k.

noncomputable def Algsuperdiff.Section4.Provider.Schauder.taylorLipschitzConst (d : ℕ) : ℝ

The constant of the Lipschitz affine competitor: 9 d / 2, the product of the truncated normalizer's slack 9 and the mean-value factor d/2.

Equations

• Algsuperdiff.Section4.Provider.Schauder.taylorLipschitzConst d = 9 / 2 * ↑d

theorem Algsuperdiff.Section4.Provider.Schauder.taylorLipschitzConst_nonneg (d : ℕ) : 0 ≤ taylorLipschitzConst d

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcess_le_taylorLipschitz {d : ℕ} (hd : d ≠ 0) {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {L : ℝ} (hL : 0 ≤ L) (hmem : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m k))) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (ExcessDecay.truncatedWindow x m k) MeasureTheory.volume) (hf : Support.HasGradientOn (ExcessDecay.truncatedWindow x m k) f G) (hG : ∀ p ∈ ExcessDecay.truncatedWindow x m k, ∀ q ∈ ExcessDecay.truncatedWindow x m k, ‖G p - G q‖ ≤ L * ‖p - q‖) : Support.affineExcess (ExcessDecay.truncatedWindow x m k) f ≤ taylorLipschitzConst d * L * 3 ^ k

The Lipschitz affine competitor, excess form.

E(f, (x+□_k) ∩ □_m) ≤ (9d/2) · L · 3^k for f whose gradient field is L-Lipschitz on the window. One full power of the scale — the improvement over ExcessDecay.affineExcess_le_taylor's half power.