CubeSchauderTopScale

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

Cube Schauder: the excess of the zero-datum solution at the top scale

CubeSchauderCampanato.affineExcess_le_campanato delivers the Campanato datum for every scale j ≤ m. The full-cube consumer (CubeSchauderAssembly.exists_zeroDatumWitness_of_campanato) runs the slope telescope at top index T = m+1, so it needs one further scale: the excess of the solution over the window at scale m+1, which by CubeSchauderPointwise.truncatedWindow_top_eq is □_m itself, independently of the base point.

This module supplies exactly that one estimate:

  E(w, □_m) ≤ C_Poincaré(d)·d · KG · √(3^m) ≤ C_Poincaré(d)·d · KG · √(3^{m+1}) .

The proof is CubeSchauderCampanato.affineExcess_initial_le run without the window transfer: freeze the forcing at G(0) (a zero-trace test function does not see a constant forcing), apply the sharp energy bound dirichletEnergy_le_of_isDivFormWeakSolutionOn_one, convert the coordinate sum by sqrt_freezing_budget, apply the Dirichlet Poincaré inequality eLpNorm_le_schauderDirichletPoincare at the inscribing cube 0 + □_m, and compare the excess against the constant competitor c = 0. Because the window is the cube itself, Support.AffineExcess.affineExcess_openCubeSet identifies the general normalizer |W|^{-1/d} with the cube normalizer 3^{-m} — no volume sandwich and no aspect-ratio loss appear, so the constant is strictly smaller than the truncated-window constant schauderInitialConst d.

References

• ABK26; Armstrong--Kuusi, Elliptic Regularity, Proposition p.Schauder.C1alpha.

1. The excess on the whole cube

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcess_openCubeSet_le {d : ℕ} [NeZero d] (hd : d ≠ 0) {m : ℤ} (u : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {KG : ℝ} (hKG : 0 ≤ KG) (hGL2 : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) G) (hG : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) KG G) (hu : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toH1Function G) : Support.affineExcess (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun ≤ schauderTopScaleConst d * KG * √(3 ^ m)

The excess of the zero-datum solution over □_m itself.

E(w, □_m) ≤ C_Poincaré(d)·d·KG·√(3^m). On the cube the general normalizer |W|^{-1/d} is 3^{-m} (affineExcess_openCubeSet), so the 3^m of the Poincaré inequality cancels exactly and no aspect-ratio constant appears.

2. The Campanato datum at the top scale, at every base point

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcess_truncatedWindow_top_le {d : ℕ} [NeZero d] (hd : d ≠ 0) {m : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {KG : ℝ} (hKG : 0 ≤ KG) (hGL2 : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) G) (hG : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) KG G) (hu : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toH1Function G) : Support.affineExcess (ExcessDecay.truncatedWindow z m (m + 1)) u.toFun ≤ schauderTopScaleConst d * KG * √(3 ^ (m + 1))

The top-scale Campanato datum, uniform in the base point.

At scale m+1 every truncated window centred in □_m is □_m itself, so the single cube estimate of affineExcess_openCubeSet_le supplies the datum at j = m+1 for every z ∈ □_m — interior and boundary base points alike. The scale is relaxed from √(3^m) to √(3^{m+1}) to meet the consumer's display.