CubeSchauderBoundaryTwin

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

Cube Schauder: the boundary twin of the Lipschitz gradient atom

CubeSchauderOneStep.exists_gradientLipschitz_interior reads the harmonic gradient atom gradField_lipschitzOn_of_harmonic at its own exponent α = 1 on the interior window family. The proved boundary producer ExcessDecay.Schauder.exists_gradientHolder_boundary_raw reads the lossy α = 1/2 corollary gradField_holderHalf_of_harmonic on the reflected window family.

The hdiam slot of the Hölder corollary disappears; nothing else changes.

The only arithmetic difference from the interior twin is the excess normalizer. On the interior window |W₂|^{-1/d} ≥ 3^{-(n-2)}; on the reflected window the partial reflections can double each side, so |W₂| ≤ (2·3^{n-2})^d and

  affineExcessRaw (reflectedWindow x m (n-2)) V
    ≤ 2 · 3^{n-2} · affineExcess (reflectedWindow x m (n-2)) V ,

which is the same factor 2 the proved exists_gradientHolder_boundary carries. The constant is therefore the interior 1296 doubled, at the boundary ratio: boundaryLipschitzWindowConst d = 2592 · schauderConst d · boundarySchauderRatioConst d.

References

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

1. The constant

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

The Lipschitz Schauder constant of the boundary branch. C(d) explicit: 2592 · schauderConst d · boundarySchauderRatioConst d, where 2592 = 2 · 4 · 324 collects the atom's factor 4, the half-radius R = 3^{n-3}/2 with the two triadic scale gaps n-3, n-2 against n, and the reflection's normalizer factor 2.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Schauder.boundaryLipschitzWindowConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ boundaryLipschitzWindowConst d

2. Two arithmetic identities

3. The reflected excess normalizer

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcessRaw_reflectedWindow_le {d : ℕ} (hd : d ≠ 0) {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hkm' : k < m) (V : HCPolySupport.Vec d → ℝ) : Support.affineExcessRaw (ExcessDecay.reflectedWindow x m k) V ≤ 2 * 3 ^ k * Support.affineExcess (ExcessDecay.reflectedWindow x m k) V

The reflected window's normalizer, one side.

|reflectedWindow x m k| ≤ (2·3^k)^d, so the unnormalized excess minimum is at most 2·3^k times the normalized one. This is the exact source of the factor 2 carried by the proved exists_gradientHolder_boundary.

4. The boundary Lipschitz atom

theorem Algsuperdiff.Section4.Provider.Schauder.exists_gradientLipschitz_boundary {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) {V : HCPolySupport.Vec d → ℝ} (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑ExcessDecay.Schauder.toEuc.symm) (⇑ExcessDecay.Schauder.toEuc '' ExcessDecay.reflectedWindow x m (n - 2))) (hintsq : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => (V y - Support.affineEval c g y) ^ 2) (ExcessDecay.reflectedWindow x m (n - 2)) MeasureTheory.volume) (p : HCPolySupport.Vec d) : p ∈ ExcessDecay.truncatedWindow x m (n - 3) → ∀ q ∈ ExcessDecay.truncatedWindow x m (n - 3), ‖ExcessDecay.Schauder.gradField V p - ExcessDecay.Schauder.gradField V q‖ ≤ boundaryLipschitzWindowConst d * 3 ^ (-n) * Support.affineExcess (ExcessDecay.reflectedWindow x m (n - 2)) V * ‖p - q‖

The harmonic gradient-Lipschitz bound on the reflected one-step window.

For V classically harmonic on the partially reflected window reflectedWindow x m (n-2), the gradient field gradField V is Lipschitz on the inner truncated window (x + □_{n-3}) ∩ □_m with constant

  boundaryLipschitzWindowConst d · 3^{-n} · E(V, reflectedWindow x m (n-2)) .

This is ExcessDecay.Schauder.exists_gradientHolder_boundary_raw with the atom read at its own exponent α = 1 instead of the lossy α = 1/2 corollary: the six geometry slots are literally the ones the proved boundary producer already feeds, and the hdiam slot is dropped.