CorrectorComposed

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

The residual corrector at the boundary datum's affine lift, composed

• the residual bound ‖h - ℓ_h‖_{L^∞(W)} ≤ 2 d [∇h]_{C^{0,1/2}} (3^k/2)^{3/2} (AffineSplitLift.abs_sub_affineLift_volumeAverage_le);
• the globally clamped H¹ datum (ResidualCorrectorExistence.exists_h1_clamp), the carrier bridge from an L^∞-bound-on-V to the global bound CoarseGraining's truncation machinery wants;
• the corrector itself with both boundary bounds (ResidualCorrectorExistence.exists_residualCorrector), and the two-sided maximum principle (BoundaryLaneMaxPrinciple.ae_abs_le_of_isWeaklyHarmonicOn).

This module composes them into the single statement the boundary lane consumes: on the anchor's own truncated window V = (x+□_k) ∩ □_m, the harmonic corrector w carrying the datum h - ℓ_h exists and satisfies

  ‖w‖_{L^∞(V)}  ≤  2 d [∇h]_{C^{0,1/2}(V)} (3^k/2)^{3/2} ,

which is the draft's e.data.residual display.

What the hypotheses are, and where they come from (disclosed)

HasGradientOn V h.toFun G and HolderSeminormBoundOn V (1/2) K G are the classical C^{1,1/2} half of the printed datum. The frozen theorem's clause (iv) supplies only h ∈ H^{1+s}, so these are inputs here, carried in the statement and not derived; the module asserts nothing about their availability. Everything else — convexity, nonemptiness, finiteness and positivity of the window volume, the diameter bound — is discharged from BoundaryLaneWindows.

References

• ABK26; the C^{1,1/2} datum.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.affineResidualLevel (d : ℕ) (K : ℝ) (k : ℤ) : ℝ

The residual level of the draft's e.data.residual, at the window (x+□_k) ∩ □_m: 2 d [∇h]_{C^{0,1/2}} (3^k/2)^{3/2}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.affineResidualLevel d K k = 2 * ↑d * K * (3 ^ k / 2) ^ (3 / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineResidualLevel_nonneg (d : ℕ) {K : ℝ} (hK : 0 ≤ K) (k : ℤ) : 0 ≤ affineResidualLevel d K k

1. The residual bound on the truncated window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_sub_affineLift_le_affineResidualLevel {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (truncatedWindow x m k) MeasureTheory.volume) (hf : Support.HasGradientOn (truncatedWindow x m k) f G) (hG : Support.HolderSeminormBoundOn (truncatedWindow x m k) (1 / 2) K G) {y : HCPolySupport.Vec d} (hy : y ∈ truncatedWindow x m k) : |f y - affineLift x (f x) (HCPolySupport.volumeAverageVec (truncatedWindow x m k) G) y| ≤ affineResidualLevel d K k

e.data.residual at the anchor's own window.

The frozen theorem's boundary datum h, restricted to the truncated window V = (x+□_k) ∩ □_m, differs from its affine lift at the average slope (∇h)_V by at most 2 d K (3^k/2)^{3/2} at every point of V.

2. The composed corrector

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_residualCorrector_affineLift {d : ℕ} [NeZero d] {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (truncatedWindow x m k) MeasureTheory.volume) (hgrad : Support.HasGradientOn (truncatedWindow x m k) h.toFun G) (hG : Support.HolderSeminormBoundOn (truncatedWindow x m k) (1 / 2) K G) : ∃ (Psi : HCPolySupport.H1Function (truncatedWindow x m k)) (w : HCPolySupport.H1Function (truncatedWindow x m k)), (∀ y ∈ truncatedWindow x m k, Psi.toFun y = h.toFun y - affineLift x (h.toFun x) (HCPolySupport.volumeAverageVec (truncatedWindow x m k) G) y) ∧ Support.IsWeaklyHarmonicOn (truncatedWindow x m k) w ∧ (HCPolySupport.MemH10 (truncatedWindow x m k) fun (y : HCPolySupport.Vec d) => w.toFun y - Psi.toFun y) ∧ ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (truncatedWindow x m k), |w.toFun y| ≤ affineResidualLevel d K k

The residual corrector of the draft's item 2(ii), composed.

On the anchor's truncated window V = (x+□_k) ∩ □_m there are an H¹(V) datum Ψ agreeing on V with h - ℓ_h and a weakly harmonic w with

• w - Ψ ∈ H¹₀(V) (the Dirichlet condition w = h - ℓ_h on ∂V), and
• |w| ≤ 2 d K (3^k/2)^{3/2} almost everywhere on V (the draft's ‖w‖_{L^∞(V)} ≤ C(d) 3^{3k/2} [∇h]_{C^{0,1/2}}).

Ψ is the clamped datum: h - ℓ_h need not be globally bounded off V, and CoarseGraining's truncation machinery asks for a global bound. On V — the only place the statement is read — Ψ and h - ℓ_h coincide, which is recorded as the first clause. Nothing else about Ψ is claimed.