CubeSchauderIteration

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

Cube Schauder: the de-randomized Campanato iteration

The recursion produced by the freezing step of CubeSchauderFreezing at the triadic sub-scales of a cube has the shape

  E (k+1) ≤ theta * E k + F * rho ^ k ,

where E k is the excess at scale 3^{-k}, theta is the contraction factor supplied by the interior (or reflected boundary) regularity of the frozen harmonic comparison function, rho = 3^{-alpha} is the freezing gain, and F is the C^{0,alpha} seminorm of the forcing. Whenever theta < rho < 1 the iteration closes at the forcing rate:

  E k ≤ (E 0 + F / (rho - theta)) * rho ^ k ,

which is exactly the Campanato bound whose Morrey dual is ∇u ∈ C^{0,alpha}.

At the development's exponent alpha = 1/2 the rate is rho = 3^{-1/2}, i.e. the 3^{-k/2} decay of the target ZeroDatumCubeSchauder.

Nothing in this module is an elliptic estimate: every declaration is an unconditional statement about real sequences, plus the triadic dictionary that identifies rho ^ k with the gauge 3^{-k/2} of the frozen conclusion.

Main results

• excess_le_of_recursion — the sharp induction: the recursion propagates the ansatz theta ^ k * + (F / (rho - theta)) * rho ^ k.
• excess_le_geometric — the Campanato form E k ≤ ( + F/(rho-theta)) rho^k.
• excess_le_geometric_triadic_half — the same at rho = 3^{-1/2}, spelled in the frozen gauge Real.rpow 3 (-(k/2)).
• excess_le_of_recursion_of_le — the degenerate-rate variant theta ≤ rho with a strict inequality only at the reabsorption step.

References

• Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), Proposition p.Schauder.C1alpha, the display e.Sch1a.1 and the dyadic geometric series preceding e.Sch1a.2.
• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. The one-step recursion, iterated

theorem Algsuperdiff.Section4.Provider.Schauder.excess_le_of_recursion {E : ℕ → ℝ} {theta rho F : ℝ} (htheta : 0 ≤ theta) (hgap : theta < rho) (hF : 0 ≤ F) (hstep : ∀ (k : ℕ), E (k + 1) ≤ theta * E k + F * rho ^ k) (k : ℕ) : E k ≤ theta ^ k * E 0 + F / (rho - theta) * rho ^ k

The Campanato induction.

If a nonnegative sequence contracts at rate theta with a forcing remainder decaying at the strictly larger rate rho, then it is dominated by the sum of the two geometric profiles, with the forcing amplified by the gap rho - theta only. This is the reabsorption at the heart of e.Sch1a.1.

theorem Algsuperdiff.Section4.Provider.Schauder.excess_le_geometric {E : ℕ → ℝ} {theta rho F : ℝ} (htheta : 0 ≤ theta) (hgap : theta < rho) (hF : 0 ≤ F) (hE0 : 0 ≤ E 0) (hstep : ∀ (k : ℕ), E (k + 1) ≤ theta * E k + F * rho ^ k) (k : ℕ) : E k ≤ (E 0 + F / (rho - theta)) * rho ^ k

The Campanato bound. The iterated recursion decays at the forcing rate rho, with amplitude E 0 + F / (rho - theta).

2. The triadic gauge

3. The sup-over-scales form