CubeSchauderClose

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

Cube Schauder: the assembly at one residue

CubeSchauderAssembly.zeroDatumCubeSchauder_of_residues reduces ZeroDatumCubeSchauder to two named residues:

• hE — the Campanato datum at every base point of □_m;
• hae — the almost-everywhere identification Ψ = ∇w.

CubeSchauderAeLimit.ae_campanatoSlopeLimit_eq_grad proves hae off hE alone. This module performs that substitution once and for all: the route now carries exactly one residue, the Campanato datum, and every other ingredient of the zero-datum core is discharged.

  hE at every z ∈ □_m, every j ≤ m+1   ⟹   ZeroDatumCubeSchauder d (zeroDatumRouteConst d C)

References

• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

theorem Algsuperdiff.Section4.Provider.Schauder.zeroDatumCubeSchauder_of_campanato {d : ℕ} (hd : 0 < d) {C : ℝ} (hC : 0 ≤ C) (hres : ∀ (m : ℤ) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (KG : ℝ), 0 ≤ KG → 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 ≤ C * KG * √(3 ^ j)) : ZeroDatumCubeSchauder d (zeroDatumRouteConst d C)

ZeroDatumCubeSchauder off the Campanato datum alone.

The a.e. identification residue of CubeSchauderAssembly.zeroDatumCubeSchauder_of_residues is discharged by CubeSchauderAeLimit.ae_campanatoSlopeLimit_eq_grad, which consumes exactly the Campanato datum that the first residue already supplies. What remains is a single hypothesis: the Campanato bound at every base point of □_m.