CubeSchauderCampanato

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

Cube Schauder: the Campanato bound of the zero-datum solution

The rate resolution, made explicit

Per triadic step of size k the two rates are

  theta_k = lipschitzContractionConst d · 3^{-k}      (the contraction)
  rho_k   = √(3^{-k})                                  (the freezing gain)

theta_k / rho_k = lipschitzContractionConst d · √(3^{-k}) → 0, so the gap is uniform as soon as k is large; schauderStepSize d is such a k (and ≥ 3, the one-step machinery's own requirement). With the C^{0,1/2} interior atom one would instead get theta_k = C(d)·√(3^{-k}) = C(d)·rho_k — no gap at any k, the Campanato exponent strictly below 1/2 and the frozen external's inclusive endpoint s ≤ 1/2 unreachable. That is why the composition is routed through the Lipschitz atom.

At the sharp gap the Campanato bound reads, on the window family W_j = (x + □_j) ∩ □_m of a point x of the interior half-cube □_{m-1},

  E(w, W_j) ≤ schauderCampanatoConst d · KG · √(3^j)     for every j ≤ m,

w the zero-datum H¹₀(□_m) solution of -Δw = ∇·G and KG the C^{0,1/2} seminorm of G — the Campanato characterization of ∇w ∈ C^{0,1/2}, with exponent exactly 1/2.

Main results

• exists_schauderStepSize / schauderStepSize / schauderStepSize_gap — the step size and the machine-checked rate gap theta < rho.
• excessDecay_oneStep_forced — the one step for the forced equation.
• affineExcess_initial_le — the excess at the top scale.
• affineExcess_le_campanato_sublattice — the iterated bound at the scales m - i·k₀.
• affineExcess_le_campanato — the same at every scale j ≤ m.

What this module does not do

It is the interior regime: the base point x is restricted to the interior half-cube □_{m-1}, which is what makes the geometry slot x + □_{j-2} ⊆ □_m of the one-step producer available at every scale.

References

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

1. Two arithmetic helpers

theorem Algsuperdiff.Section4.Provider.Schauder.sqrt_pow_nat {t : ℝ} (ht : 0 ≤ t) (i : ℕ) : √(t ^ i) = √t ^ i

√(t^i) = (√t)^i.

theorem Algsuperdiff.Section4.Provider.Schauder.zpow_sub_mul_step (m : ℤ) (k i : ℕ) : 3 ^ (m - ↑i * ↑k) = 3 ^ m * (3 ^ (-↑k)) ^ i

The triadic scale at step i of the iteration factorizes.

4. The excess at the top scale

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

The constant of the top-scale excess: 9 · √((3²)^d) · C_Poincaré(d) · d.

Equations

• Algsuperdiff.Section4.Provider.Schauder.schauderInitialConst d = 9 * √((3 ^ 2) ^ d) * (Algsuperdiff.Section4.Provider.Schauder.schauderDirichletPoincareConst d * ↑d)

theorem Algsuperdiff.Section4.Provider.Schauder.schauderInitialConst_nonneg (d : ℕ) : 0 ≤ schauderInitialConst d

1. The constant

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

The top-scale constant C_Poincaré(d)·d.

Equations

• Algsuperdiff.Section4.Provider.Schauder.schauderTopScaleConst d = Algsuperdiff.Section4.Provider.Schauder.schauderDirichletPoincareConst d * ↑d

theorem Algsuperdiff.Section4.Provider.Schauder.schauderTopScaleConst_nonneg (d : ℕ) : 0 ≤ schauderTopScaleConst d

2. The normalized L² bound on the whole cube

theorem Algsuperdiff.Section4.Provider.Schauder.normalizedL2On_le_of_isDivFormWeakSolutionOn_one {d : ℕ} [NeZero 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.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun ≤ schauderTopScaleConst d * KG * (3 ^ m * √(3 ^ m))

The zero-datum solution is small in L²(□_m).

Freezing the forcing at G(0), the sharp energy bound and the Dirichlet Poincaré inequality give

  ‖w‖_{L²(□_m)} ≤ C_Poincaré(d)·d·KG·3^m·√(3^m) .

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcess_initial_le {d : ℕ} [NeZero d] (hd : d ≠ 0) {m : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ 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 x m m) u.toFun ≤ schauderInitialConst d * KG * √(3 ^ m)

The excess of the zero-datum solution at the top scale.

E(w, (x+□_m) ∩ □_m) ≤ schauderInitialConst d · KG · √(3^m). The proof is the freezing identity at the constant G(0) (a zero-trace test function does not see a constant forcing), the sharp energy bound, the coordinate dictionary and the Dirichlet Poincaré inequality — the same four steps as the one-step residue, run once at the top scale.