CubeSchauderBoundaryCampanato #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: the Campanato bound at every base point of □_m #
The boundary mirror of CubeSchauderCampanato. The interior module's chain is
reproduced verbatim with one substitution: the interior one step
(excessDecay_oneStep_lipschitz, which needs the geometry slot
x + □_{n-2} ⊆ □_m and therefore the interior half-cube) is replaced by the
boundary one step (excessDecay_oneStep_boundary_lipschitz, which needs only
x ∈ □_m and n - 2 < m). Everything else — the rate gap, the geometric
recursion CubeSchauderIteration.excess_le_geometric, the top-scale estimate
CubeSchauderCampanato.affineExcess_initial_le (already stated at every base
point of □_m), and the sub-lattice-to-every-scale interpolation — is reused
unchanged.
This is the structural point: the boundary route carries no
interior slot, so one branch supplies the Campanato datum at every base
point, and the interior restriction x ∈ □_{m-1} disappears from the endpoint.
E(w, (x + □_j) ∩ □_m) ≤ boundaryCampanatoFullConst d · KG · √(3^j)
for every x ∈ □_m and every j ≤ m.
References #
- Armstrong--Kuusi, Elliptic Regularity (
ellipticregularity.tex), Propositionp.Schauder.C1alpha, displayse.Sch1a.1--e.Sch1a.2. - ABK26;
Algsuperdiff/Frozen/External/CubeSchauder.lean.
1. The step size and the rate gap #
The boundary rate gap exists. There is a step size k ≥ 3 at which the
boundary contraction rate C_contr(d)·3^{-k} is strictly below the freezing rate
√(3^{-k}). The proof is the interior argument at the boundary constant.
The step size of the boundary Campanato iteration, k₀^∂(d).
Instances For
The boundary rate gap, machine-checked.
2. The one step for the forced equation, at any base point #
The boundary one step, forced.
For the zero-datum solution u of -Δu = ∇·G on □_m with
[G]_{C^{0,1/2}} ≤ KG, at any base point x ∈ □_m and any scale n with
n - 1 ≤ m:
E(u, W_{n-k}) ≤ C_contr(d)·3^{-k}·E(u, W_n) + C_rem(d,k)·C_res(d)·KG·√(3ⁿ) .
3. The Campanato bound #
The boundary Campanato constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The boundary Campanato bound on the triadic sub-lattice, at every base
point of □_m.
4. Every scale, every base point #
The full-range boundary Campanato constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Campanato bound at every scale and every base point of □_m.
For the zero-datum solution w of -Δw = ∇·G on □_m with
[G]_{C^{0,1/2}(□_m)} ≤ KG, at every x ∈ □_m and every j ≤ m,
E(w, (x + □_j) ∩ □_m) ≤ boundaryCampanatoFullConst d · KG · √(3^j) .
The interior restriction of CubeSchauderCampanato.affineExcess_le_campanato is
gone: the reflected competitor needs no room inside the cube.