StepFourBoundaryDecayC1

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

1. The boundary δ in the α-free three-leg grouping

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFourBoundaryDeltaC1 {d : ℕ} (M : Section3.ABKModel d) (Cbd Cah Khinf Kg Kh epsj : ℝ) (p : ℤ) : ℝ

The boundary Step-4 output, three-leg grouping.

A^g_p + (A^h_p + ε_j·H) with H = 2 C_bd K_{h,∞}: the α-free shape, with the ∇h flat leg ε-funded and no ε-free summand.

Equations

• One or more equations did not get rendered due to their size.

2. The two restrictions of the root's datum binders

theorem Algsuperdiff.Section4.Provider.Regularity.hasGradientOn_truncatedWindow_of_root {d : ℕ} {m p : ℤ} {z : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f G) : Support.HasGradientOn (ExcessDecay.truncatedWindow z m p) f G

The classical C¹ half descends to a truncated window. The root's binder, restricted to the corrector's carrier (one carrier only: Support.HasGradientOn).

theorem Algsuperdiff.Section4.Provider.Regularity.norm_volumeAverageVec_le_of_root_sup {d : ℕ} {m p : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {Kh : ℝ} (hKh : 0 ≤ Kh) (hsup : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) : ‖HCPolySupport.volumeAverageVec (ExcessDecay.truncatedWindow z m p) hdat.grad‖ ≤ Real.rpow 3 (↑m / 2) * Kh

3. hstep4 on the boundary branch

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourDecay_boundary_pinned (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Ccap : ℝ) (Cb : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Ccap ∧ 0 ≤ Cb ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → ∀ delta ∈ Set.Ioc 0 (1 / 2), delta ≤ 64 * (C ^ 2)⁻¹ * stepOneS ^ 6 → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k * Ccap * stepOneS.rpow (-3) * √delta ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1)) → ∀ (L m : ℤ), m ≤ L → m ≤ m0 → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ (n : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), 0 ≤ Kg → 0 ≤ Kh → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh hdat.grad → (∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) hdat.toFun hdat.grad → ∀ (c : ℤ → ℝ) (slope : ℤ → HCPolySupport.Vec d), (∀ j ≤ m, Support.IsAffineMinimizer (stepThreeWindow z m j) u.toFun (c j) (slope j)) → ∀ (j : ℤ), n + (↑k + 1) ≤ j → j ≤ m - 1 → ⋯

hstep4 on the boundary branch, discharged.

For one omega, every centre z ∈ □_m (NO interiority, NO lattice condition) and every scale j ∈ [n+k+1, m-1] outside the Step-3 bad set 𝓑_z, the Step-4 per-scale excess decay at the concrete windows U_j = stepThreeWindow z m j, the Step-5 slot ε_j (times the slot's own coefficient) and the boundary three-leg δ^∂_{j-1}.

Every hypothesis is either the trimmed slot's own, the annular producer's own, or a binder of the root's printed datum block; there is no harmonic-approximation hypothesis, no competitor package, no MemLp residue and no interiority.

4. The boundary δ-budget over the iteration window

theorem Algsuperdiff.Section4.Provider.Regularity.sum_Icc_top_stepFourBoundaryDeltaC1_le {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) (hgamma : M.gamma < 1 / 2) {Cbd Cah Khinf Kg Kh Se delta : ℝ} {n m : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (hnm : n ≤ m) (hm : m ≤ m0) (hCbd : 0 ≤ Cbd) (hCah : 0 ≤ Cah) (hKhinf : 0 ≤ Khinf) (hKg : 0 ≤ Kg) (hKh : 0 ≤ Kh) (hSe : ∑ j ∈ Finset.Icc n m, stepFiveEps M j z delta omega ≤ Se) : ∑ j ∈ Finset.Icc n m, stepFourBoundaryDeltaC1 M Cbd Cah Khinf Kg Kh (stepFiveEps M j z delta omega) (j - 1) ≤ edFinalDataG M Cbd Kg m + (Cah * (3 ^ (↑m / 2) * Kh) / (1 - stepFiveRatioH) + Se * (2 * Cbd * Khinf))

e.sum.delta.j.bound for the boundary family.

The window sum of stepFourBoundaryDeltaC1 at the slot's own index shift, in the α-free grouping dataG + dataH_∂:

   ∑_{j=n}^{m} δ^∂_{j-1}
     ≤ edFinalDataG(C_bd, K_g)  +  ( C_ah 3^{m/2} K_h / (1-r₂)  +  S_ε·(2 C_bd K_{h,∞}) ) ,

with r₂ = 3^{-1/2} and NO W-linear summand — the ∇h flat leg is ε-funded, so's α-free absorption StepSixBoundaryEndpoint.stepSixBoundary_holderBound_ epsFunded consumes dataH_∂ directly.