CubeSchauderAssembly

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

Cube Schauder: the representative rebuild and the zero-datum assembly

ZeroDatumCubeSchauder d C0 bounds the H¹ witness's own grad field pointwise, and an H¹ gradient is only defined almost everywhere. The existential in the statement is therefore load-bearing: one must rebuild the witness so that its grad field is the continuous representative produced by CubeSchauderPointwise.campanatoSlopeLimit.

This module does exactly that, and then assembles the two displays:

• exists_h10Function_grad_eq — the rebuild. An H¹₀ witness may have its grad field replaced by any almost-everywhere equal field: L² membership, the weak-gradient identity and the smooth-approximation package are all invariant under modification on a null set.
• exists_mem_norm_le_of_energy — the sharp energy bound gives a point of the cube where the representative is small.
• exists_zeroDatumWitness_of_campanato — the two displays of the zero-datum core, from the Campanato datum on all of □_m plus the a.e. identification of the limit field with the witness's gradient.

The two residues, named

exists_zeroDatumWitness_of_campanato carries exactly two mathematical hypotheses, both displayed in its own statement:

• hE — the Campanato bound at every base point of □_m (not only the interior half-cube □_{m-1} that CubeSchauderCampanato.affineExcess_le_campanato reaches). The boundary regime is what supplies it.
• hae — the almost-everywhere identification Ψ = ∇w.

Neither is proved here. This module is a conditional A: it proves that the two residues suffice for ZeroDatumCubeSchauder, and nothing else.

The sup bound without Poincaré

The L^∞ leg is obtained from the C^{0,1/2} bound plus one point of the cube where the field is small, and that point comes from the sharp Dirichlet energy estimate dirichletEnergy_le_of_isDivFormWeakSolutionOn_one alone: a continuous field that exceeds A everywhere would force the energy above A²|□_m|. No Poincaré inequality and no bound on the top-scale minimizer slope are needed.

References

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

1. The representative rebuild

theorem Algsuperdiff.Section4.Provider.Schauder.exists_h10Function_grad_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H10Function U) {Psi : HCPolySupport.Vec d → HCPolySupport.Vec d} (hae : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, Psi y = w.grad y) : ∃ (w' : HCPolySupport.H10Function U), w'.toFun = w.toFun ∧ w'.grad = Psi

The H¹₀ witness may be rebuilt on an almost-everywhere equal gradient field.

Every field of H10Function is invariant under modification of grad on a null set: gradMemL2 by MemLp.ae_eq, hasWeakGradient because its right-hand side is an integral, and tendsto_approx_grad because eLpNorm is an almost-everywhere invariant. The function itself is untouched.

2. A small value of the representative from the energy

theorem Algsuperdiff.Section4.Provider.Schauder.sq_norm_le_vecNormSq {d : ℕ} (v : HCPolySupport.Vec d) : ‖v‖ ^ 2 ≤ HCPolySupport.vecNormSq v

The coordinate norm dominates the ambient sup norm squared.

theorem Algsuperdiff.Section4.Provider.Schauder.exists_mem_norm_le_of_energy {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUmeas : MeasurableSet U) (hUpos : 0 < (MeasureTheory.volume U).toReal) (hUtop : MeasureTheory.volume U ≠ ⊤) {F Psi : HCPolySupport.Vec d → HCPolySupport.Vec d} (hint : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (F y)) U MeasureTheory.volume) (hae : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, Psi y = F y) {A : ℝ} (hA : 0 ≤ A) (hM : ∫ (y : HCPolySupport.Vec d) in U, HCPolySupport.vecNormSq (F y) ≤ A ^ 2 * (MeasureTheory.volume U).toReal) {delta : ℝ} (hdelta : 0 < delta) : ∃ y ∈ U, ‖Psi y‖ ≤ A + delta

A point where the representative is small.

If the Dirichlet energy of F on U is at most A²|U| and Psi = F almost everywhere on U, then Psi comes within δ of A somewhere on U, for every δ > 0.

3. The scale dictionary

theorem Algsuperdiff.Section4.Provider.Schauder.sqrt_zpow_eq_rpow_half (m : ℤ) : √(3 ^ m) = Real.rpow 3 (↑m / 2)

√(3^m) = 3^{m/2} in the frozen statement's rpow shape.

4. The zero-datum witness

theorem Algsuperdiff.Section4.Provider.Schauder.exists_zeroDatumWitness_of_campanato {d : ℕ} (hd : 0 < d) {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))) (hw : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) w.toH1Function G) {K : ℝ} (hK : 0 ≤ K) (hE : ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ j ≤ m + 1, Support.affineExcess (ExcessDecay.truncatedWindow z m j) w.toFun ≤ K * √(3 ^ j)) (hae : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), campanatoSlopeLimit m (m + 1) w.toFun y = w.grad y) : ∃ (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 ∧ (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖w'.grad x‖ ≤ (√(3 * ↑d) * KG + √3 * (campanatoHolderConst d * K)) * Real.rpow 3 (↑m / 2)) ∧ Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) (campanatoHolderConst d * K) w'.grad

The two displays of the zero-datum core, off the two named residues.

From the Campanato datum hE at every base point of □_m and the almost-everywhere identification hae, the solution w may be rebuilt so that its own gradient field is C^{0,1/2} with constant campanatoHolderConst d · K and bounded by (√(3d) · KG + √3 · campanatoHolderConst d · K) · 3^{m/2}.

Both hypotheses are displayed; nothing about them is claimed here.

5. The zero-datum core off the two residues

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

The constant delivered by the route: √(3d) + (√3 + 1)·campanatoHolderConst d·C.

Equations

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

theorem Algsuperdiff.Section4.Provider.Schauder.zeroDatumRouteConst_nonneg (d : ℕ) {C : ℝ} (hC : 0 ≤ C) : 0 ≤ zeroDatumRouteConst d C

theorem Algsuperdiff.Section4.Provider.Schauder.zeroDatumCubeSchauder_of_residues {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)) ∧ ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), campanatoSlopeLimit m (m + 1) w.toFun y = w.grad y) : ZeroDatumCubeSchauder d (zeroDatumRouteConst d C)

ZeroDatumCubeSchauder off the two named residues.

If, at every scale and every C^{0,1/2} forcing, the zero-datum solution can be produced together with (i) the Campanato bound at every base point of □_m and (ii) the almost-everywhere identification of its gradient with the limit field, then the zero-datum cube Schauder core holds at the explicit constant zeroDatumRouteConst d C.

Both residues are hypotheses of this statement; nothing about them is claimed here. This is the exact reduction the route delivers.