CubeSchauderResidue

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

Cube Schauder: the harmonic competitor and its forcing residue

The interior one step of CubeSchauderOneStep consumes two things: a competitor v harmonic on the window, and a bound on the L² distance ‖u - v‖. This module produces both, from the freezing step and Weyl's lemma, for the forced equation -Δu = ∇·G with G ∈ C^{0,1/2}.

The chain, on the window W = (x + □_n) ∩ □_m:

1. freezing (CubeSchauderFreezing.exists_frozenHarmonicReplacement, at the base point x and the constant c = G(x)): a corrector w ∈ H¹₀(W) with u - w weakly harmonic and ∫_W |∇w|² ≤ ∫_W |G - G(x)|² ≤ d KG² 3ⁿ |W| — the freezing gain, one half-power of the scale;
2. the coordinate dictionary (CubeSchauderFreezingResidue.sum_toReal_eLpNorm_grad_le_of_dirichletEnergy_le): Σᵢ ‖∂ᵢw‖_{L²(W)} ≤ d KG √(3ⁿ|W|);
3. the Dirichlet Poincaré (CubeSchauderPoincare, at the inscribing cube `x
   • □n): ‖w‖{L²(W)} ≤ C_ⁿ Σᵢ ‖∂ᵢw‖{L²(W)}, hence after dividing by |W|^{1/2}, ‖w‖{L²(W)} ≤ C_P d KG 3ⁿ √(3ⁿ)`;
4. Weyl (ExcessDecay.Schauder.exists_harmonicRepresentative_memLp): a genuine classically harmonic representative v of u - w, so that u - v = w almost everywhere on W.

The output is exactly the remainder slot of excessDecay_oneStep_lipschitz:

  3^{-n} · ‖u - v‖_{L²((x+□_{n-2}) ∩ □_m)} ≤ C_res(d) · KG · √(3ⁿ) .

The √(3ⁿ) is the whole point: the remainder decays at 3^{-1/2} per triadic scale, while the one step contracts at 3^{-1} per scale — the gap the Campanato iteration needs.

Main results

• exists_frozenHarmonicReplacement_truncatedWindow — steps 1--2.
• schauderResidueConst — √((3⁴)^d) · C_P(d) · d.
• exists_harmonicCompetitor_residue — the whole chain.

References

• Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), the harmonic-approximation display e.harmapprox.Sch.onealpha.
• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. Two small dictionary lemmas

theorem Algsuperdiff.Section4.Provider.Schauder.normalizedL2On_congr_ae {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (h : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict W, f y = g y) : Support.normalizedL2On W f = Support.normalizedL2On W g

‖·‖_{L²(W)} only sees the almost-everywhere class on W.

theorem Algsuperdiff.Section4.Provider.Schauder.vecNormSq_sub_le_of_holderSeminormBoundOn_truncatedWindow {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {KG : ℝ} (hKG : 0 ≤ KG) (hG : Support.HolderSeminormBoundOn (ExcessDecay.truncatedWindow x m n) (1 / 2) KG G) {p : HCPolySupport.Vec d} (hp : p ∈ ExcessDecay.truncatedWindow x m n) {q : HCPolySupport.Vec d} (hq : q ∈ ExcessDecay.truncatedWindow x m n) : HCPolySupport.vecNormSq (G p - G q) ≤ ↑d * (KG ^ 2 * 3 ^ n)

The oscillation of a C^{0,1/2} field on a truncated window.

2. The freezing step on a truncated window

theorem Algsuperdiff.Section4.Provider.Schauder.exists_frozenHarmonicReplacement_truncatedWindow {d : ℕ} [NeZero d] {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u : HCPolySupport.H1Function (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 G) : ∃ (w : HCPolySupport.H10Function (ExcessDecay.truncatedWindow x m n)), Support.IsWeaklyHarmonicOn (ExcessDecay.truncatedWindow x m n) (u.restrict ⋯ ⋯ - w.toH1Function) ∧ ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => w.grad y i) 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m n))).toReal ≤ ↑d * KG * √(3 ^ n * (MeasureTheory.volume (ExcessDecay.truncatedWindow x m n)).toReal)

The freezing step on the one-step window, with the gain in coordinate L² form.

If u solves -Δu = ∇·G on □_m and [G]_{C^{0,1/2}(□_m)} ≤ KG, then on the window W = (x + □_n) ∩ □_m there is a corrector w ∈ H¹₀(W) making u - w weakly harmonic and obeying

  Σᵢ ‖∂ᵢ w‖_{L²(W)} ≤ d · KG · √(3ⁿ · |W|) .

3. The residue constant and the full chain