CubeSchauderSeal

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

Cube Schauder: the zero-datum core, unconditional

CubeSchauderClose.zeroDatumCubeSchauder_of_campanato reduced the zero-datum core to a single residue: the Campanato datum

  E(w, (z + □_j) ∩ □_m) ≤ C · KG · √(3^j)   for every z ∈ □_m and every j ≤ m+1,

together with the existence of the zero-datum solution w. This module discharges it and therefore makes ZeroDatumCubeSchauder unconditional beyond the dimension hypothesis.

Three proved legs meet:

• existence — CubeSchauderFreezing.exists_h10_isDivFormWeakSolutionOn_one (CoarseGraining's zero-trace Dirichlet solvability at the identity coefficient field);
• the scales j ≤ m — CubeSchauderBoundaryCampanato.affineExcess_le_boundaryCampanato, the Campanato bound at every base point of □_m;
• the scale j = m+1 — CubeSchauderTopScale.affineExcess_truncatedWindow_top_le, where the window is the cube itself and the base point plays no role.

References

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

1. The Campanato constant of the full base-point range

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

The Campanato constant covering every base point of □_m and every scale j ≤ m+1: the boundary-route constant of the scales j ≤ m plus the top-scale constant of j = m+1.

Equations

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

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

2. The residue, discharged

theorem Algsuperdiff.Section4.Provider.Schauder.exists_zeroDatumSolution_campanato {d : ℕ} [NeZero d] (hd : d ≠ 0) (m : ℤ) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (KG : ℝ) (hKG : 0 ≤ KG) (hG : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) KG G) : ∃ (w : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) w.toH1Function G ∧ ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ j ≤ m + 1, Support.affineExcess (ExcessDecay.truncatedWindow z m j) w.toFun ≤ zeroDatumCampanatoConst d * KG * √(3 ^ j)

The Campanato residue of the route, proved.

For every scale m and every C^{0,1/2} forcing G on □_m there is a zero-datum solution w ∈ H¹₀(□_m) of -Δw = ∇·G whose excess obeys the Campanato bound at every base point of □_m and every scale j ≤ m+1.

This is exactly the hypothesis of CubeSchauderClose.zeroDatumCubeSchauder_of_campanato.

3. The zero-datum core

theorem Algsuperdiff.Section4.Provider.Schauder.zeroDatumCubeSchauder_unconditional {d : ℕ} [NeZero d] : ZeroDatumCubeSchauder d (zeroDatumRouteConst d (zeroDatumCampanatoConst d))

The zero-datum cube Schauder core, unconditional.

ZeroDatumCubeSchauder d C₀ at the explicit constant

  C₀(d) = zeroDatumRouteConst d (zeroDatumCampanatoConst d) ,

with no hypothesis beyond 0 < d.