CubeSchauderPointwise #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: from the Campanato bound to a pointwise C^{0,1/2} slope field #
E(u, (z+□_j) ∩ □_m) ≤ K · √(3^j) for every z ∈ S and every j ≤ m+1 .
From it we build the continuous slope field
Ψ(z) := lim_{j → -∞} ∇ℓ(u, (z+□_j) ∩ □_m)
and prove the two displays the cube Schauder core needs about it: a C^{0,1/2}
seminorm bound with a d-constant times K, and a sup bound at the top scale.
Why the family is Cauchy, and why no chaining lemma is needed #
CubeSchauderSlope.slopeMagnitude_windowSlope_sub_le bounds the slope
increment by the two excesses, so consecutive slopes differ by at most
2·C_stab·K·√(3^j) — a geometric sequence of ratio √(1/3), whence mathlib's
cauchySeq_of_le_geometric and dist_le_of_le_geometric_of_tendsto give the
limit and its tail estimate in two lines each.
For the two-point estimate the usual Campanato argument runs a local Hölder
bound (valid only for nearby points) and then chains it along segments of a
convex set. That chaining step is not needed here: at the top scale
j = m+1 every window (z+□_{m+1}) ∩ □_m is the same set □_m, so all the
slopes coincide there and the far-apart case is closed by two tail estimates
alone. This is what makes the module short.
Main results #
campanatoSlopeLimit— the fieldΨ, defined bylimUnder(junk value off the Cauchy locus, no subtype, no bundled choice).campanatoSlopeLimit_tail—|∇ℓ_j − Ψ| ≤ C(d)·K·√(3^j)at everyj ≤ m+1.holderSeminormBoundOn_campanatoSlopeLimit— theC^{0,1/2}bound.norm_campanatoSlopeLimit_le— the sup bound off the top-scale slope.
References #
- ABK26; Armstrong--Kuusi, Elliptic Regularity, Proposition
p.Schauder.C1alpha.
1. Two window identities #
At scale m+1 every truncated window centred in □_m is □_m.
A window at a nearby centre and one scale down sits inside the window at
x: if ‖x − y‖ < 3^k then (y+□_k) ∩ □_m ⊆ (x+□_{k+1}) ∩ □_m.
Two points of □_m are less than 3^m apart in the ambient sup norm.
2. The Campanato constants #
The geometric ratio of the slope telescope: √(1/3).
Equations
Instances For
The slope-stability constant of the truncated window family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tail constant of the slope telescope: 2·C_stab/(1 − √(1/3)).
Equations
Instances For
3. The one-step slope increment #
The slope increment at one triadic step.
Under the Campanato datum the slopes on consecutive windows about the same
centre differ by at most 2·C_stab(d)·K·√(3^j).
4. The limit field #
The Campanato slope field. Ψ(z) is the limit of the affine-minimizer
slopes of u on the windows (z+□_{T-n}) ∩ □_m as n → ∞. The top index T
is a parameter: the interior regime runs it at T = m (the range of
CubeSchauderCampanato.affineExcess_le_campanato), the full-cube regime at
T = m+1, where every window degenerates to □_m.
Equations
- Algsuperdiff.Section4.Provider.Schauder.campanatoSlopeLimit m T u z = Filter.atTop.limUnder fun (n : ℕ) => Algsuperdiff.Section4.Provider.Schauder.windowSlope m u z (T - ↑n)
Instances For
The geometric step bound of the reindexed slope sequence.
The reindexed slope sequence is Cauchy.
The tail estimate. At every scale j ≤ T the slope of the window at
scale j is within C_tail(d)·K·√(3^j) of the limit.
5. The top scale #
6. The two-point estimate #
The Hölder constant of the slope field: √3·(2·C_tail + 2·C_stab·(1 + √3)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The C^{0,1/2} bound of the slope field.
If the Campanato datum holds at every point of S ⊆ □_m up to the top scale T
with constant K, and S has diameter below 3^{T-1}, then
‖Ψ(x) − Ψ(y)‖ ≤ campanatoHolderConst d · K · ‖x − y‖^{1/2}
for all x, y ∈ S. No convexity of S and no chaining are needed: for far
apart points the two windows at scale T-1 sit inside the common window
(x+□_T) ∩ □_m, which closes the case with two tails and two slope
comparisons.