OneStepSchauderChain

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

The excess-decay one-step contraction with the Schauder gradient-Hölder estimate

discharged (interior branch)

OneStepConditional.excessDecay_oneStep_of_harmonicApprox carries two open inputs: hharm (the harmonic-approximation anchor, transcribed) and the four-slot package hint / hgrad / hhol / hschauder, i.e. the Schauder gradient-Hölder estimate. OneStepSchauderProducer.exists_gradientHolder_interior proves the second one on the interior branch.

The Schauder constant is now a definite closed-form dimensional constant,

  Csch = schauderWindowConst d = 48 · 3^{3/2} · schauderConst d · √((12(d+1))^d) ,
  schauderConst d = d · C_native(d) ,

and the boundary-datum leg is K_h = 0.

What is still assumed about the competitor

hharmclass: the competitor v is classically harmonic on the replacement window (x + □_{n-2}) ∩ □_m (Mathlib's InnerProductSpace.HarmonicOnNhd, transported across toEuc). The producer of the competitor (ResidualCorrectorExistence) delivers the variational Support.IsWeaklyHarmonicOn; OneStepSchauderWeyl bridges variational to classical for the CoarseGraining convex smoothings of the competitor, at the full radius.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_interior_of_harmonicApprox {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {M : Section3.ABKModel d} {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {delta : ℝ} (hdelta1 : delta ≤ 1) {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {u v : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) (huv : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => u y - v y) 2 (MeasureTheory.volume.restrict (movedReplacementCube x m n))) (hharmclass : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑Schauder.toEuc.symm) (⇑Schauder.toEuc '' truncatedWindow x m (n - 2))) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (s / 8 * √delta)) {B : ENNReal} (hB : B ≠ ⊤) (hharm : (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (1 / 2)).indicator (fun (_omega' : Section3.Cutoff.CutoffSample d) => MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u y - v y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))))) omega ≤ B) : Support.affineExcess (truncatedWindow x m (n - ↑k)) u ≤ taylorContractionConst d * Schauder.schauderWindowConst d * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d (Schauder.schauderWindowConst d) k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * B.toReal)) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * 0

The one-step excess-decay contraction on the interior branch, with the gradient-Hölder Schauder estimate discharged.

Identical to excessDecay_oneStep_of_harmonicApprox except that the four Schauder slots are replaced by classical harmonicity of the competitor on the replacement window; the constant is Csch = schauderWindowConst d and the boundary-datum leg is K_h = 0.