StepFourFinalInterior

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

hstep4's body at one scale, on the interior branch

What this module is

excessDecay_oneStep_interior_anchored_twoLeg is the one-step contraction off the harmonic-approximation anchor's frontier-empty clause: two legs, no ∇h, the oscillation on the contraction's own window. stepFourDecay_of_edOneStep is the Step-4 collapse into hstep4's body. This module composes them at x := z, with the carried items discharged from EdFinalInputs, and produces

   E(u, U_{n-k}) ≤ 3^{-k/4} E(u, U_n) + C_ε ε_n |∇ℓ_n| + δ_n ,
   U_j = stepThreeWindow z m j = (z + □_j) ∩ □_m ,
   δ_n = C_δ 3^{n/2} σ_n^{-1} K_g .

δ_n is the g-leg shape of the Step-5 family, at the root's own Hölder datum K_g in place of the W^{1/2,∞} seminorm (which it dominates). The ungated, non-decaying flat ∇h leg is gone: the interior clause carries no ∇h leg at all.

The three conversions, per leg

• the 𝓔-leg: the oscillation-to-excess fold is oscLeg_normalized_le_interior — a theorem at this window, not a binder;
• the Gagliardo exponent: StepFourCollapseInterface.stepFourGsemLeg_le is read at the interior clause's OWN window index n and re-pinned to the collapse's n+1 by Real.rpow_le_rpow_of_exponent_le — the one-scale re-pin is free because 1/2 - s > 0.

References

• ABK26, l.excess.decay.good.scales; l.harmonic.approximation.good.scales, (interior clause); t.regularity Step 4.

1. The interior branch's ε coefficient and δ family

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalEpsCoeff (d : ℕ) [NeZero d] (C : ℝ) (k : ℕ) (s : ℝ) : ℝ

The ε-slot coefficient the interior collapse produces: C_rem √((3²)^d) C s^{-4} C_i(d) (stepFourEpsCoeff at the interior constants).

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalEpsCoeff_nonneg (d : ℕ) [NeZero d] {C : ℝ} (hC : 0 ≤ C) (k : ℕ) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ edFinalEpsCoeff d C k s

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalDeltaConst (d : ℕ) [NeZero d] (C : ℝ) (k : ℕ) (s : ℝ) : ℝ

The δ-slot constant the interior collapse produces: 8 C_rem √((3²)^d) C s^{-19/2}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalDelta {d : ℕ} (M : Section3.ABKModel d) (Cdel Kg : ℝ) (n : ℤ) : ℝ

The interior branch's δ_n: C_δ 3^{n/2} σ_n^{-1} K_g, the g-leg of the Step-5 family at the root's own Hölder datum. There is no ∇h leg and no boundary indicator.

Equations

• Algsuperdiff.Section4.Provider.Regularity.edFinalDelta M Cdel Kg n = Cdel * 3 ^ (↑n / 2) * (↑(Algsuperdiff.Section3.Annealed.sigmaBar M n))⁻¹ * Kg

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDelta_nonneg {d : ℕ} {M : Section3.ABKModel d} {Cdel Kg : ℝ} (hC : 0 ≤ Cdel) (hK : 0 ≤ Kg) (n : ℤ) : 0 ≤ edFinalDelta M Cdel Kg n

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourDeltaOut_interior_eq {d : ℕ} {M : Section3.ABKModel d} {C s epsj Kg : ℝ} [NeZero d] (hs : 0 < s) (k : ℕ) (n : ℤ) : stepFourDeltaOut (ExcessDecay.triangleRemainderConst d (ExcessDecay.Schauder.schauderWindowConst d) k) (√((3 ^ 2) ^ d)) C s epsj 0 (s ^ (-(5 / 2)) * (↑(Section3.Annealed.sigmaBar M n))⁻¹) Kg 0 n = edFinalDelta M (edFinalDeltaConst d C k s) Kg n

The produced δ at the interior instantiation (no ∇h legs) is edFinalDelta. The identity is s^{-7} · s^{-5/2} = s^{-19/2}.

theorem Algsuperdiff.Section4.Provider.Regularity.twoLeg_is_hed {s : ℝ} (hs : 0 < s) (C Efl Osc Gsem SigInv2 Crem Vd : ℝ) (n : ℤ) : Crem * (3 ^ (-n) * (Vd * (C * s.rpow (-4) * Efl * Osc + C * s.rpow (-(19 / 2)) * SigInv2 * Real.rpow 3 ((1 + s) * ↑(n - 2)) * Gsem))) = Crem * (3 ^ (-n) * (Vd * (C * s ^ (-4) * Efl * (Osc + s ^ (-(3 / 2)) * 3 ^ ↑(n - 2) * 0) + C * s ^ (-7) * (s ^ (-(5 / 2)) * SigInv2) * 3 ^ ((1 + s) * ↑(n - 2)) * Gsem + C * s ^ (-6) * 3 ^ ((1 + s) * ↑(n - 2)) * 0 + C * s ^ (-6) * 3 ^ ↑(n - 2) * 0)))

The interior two-leg display IS's hed slot at Gav = Hsem = Hl2 = 0 and SigInv = s^{-5/2} σ_{n-2}^{-1}: the single s-power carries the interior clause's -19/2 force exponent into the collapse's s^{-7} shom slot. One rpow_add identity, no inequality.

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourDecay_of_twoLegDisplay {d : ℕ} [NeZero d] {Exc Slp : ℤ → ℝ} {n : ℤ} {k : ℕ} {Crem Vd C s Efl Osc Gsem SigInv2 SigInvN2 epsj Kg thetaK : ℝ} (hCV : 0 ≤ Crem * Vd) (hs : 0 < s) (hcoef4 : 0 ≤ C * s ^ (-4)) (hcoef6 : 0 ≤ C * s ^ (-6)) (hcoef7 : 0 ≤ C * s ^ (-7)) (hw : 0 ≤ s ^ (-(3 / 2))) (hExc0 : 0 ≤ Exc n) (hEfl : Efl ≤ epsj) (heps0 : 0 ≤ epsj) (hOsc0 : 0 ≤ 3 ^ (-n) * Osc) (hOsc : 3 ^ (-n) * Osc ≤ ExcessDecay.endpointConst d (1 / 9) * (Exc n + Slp n)) (hSig : s ^ (-(5 / 2)) * SigInv2 ≤ 8 * (s ^ (-(5 / 2)) * SigInvN2)) (hSigN0 : 0 ≤ s ^ (-(5 / 2)) * SigInvN2) (hGsem0 : 0 ≤ Gsem) (hKg0 : 0 ≤ Kg) (hGsem : Gsem ≤ Kg * 3 ^ (↑(n + 1) * (1 / 2 - s))) (hCcon : ExcessDecay.taylorContractionConst d * ExcessDecay.Schauder.schauderWindowConst d * ExcessDecay.windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) ≤ thetaK / 2) (hTC34B : stepFourEpsCoeff Crem Vd C s (ExcessDecay.endpointConst d (1 / 9)) * epsj ≤ thetaK / 2) (hed : Exc (n - ↑k) ≤ ExcessDecay.taylorContractionConst d * ExcessDecay.Schauder.schauderWindowConst d * ExcessDecay.windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Exc n + Crem * (3 ^ (-n) * (Vd * (C * s.rpow (-4) * Efl * Osc + C * s.rpow (-(19 / 2)) * SigInv2 * Real.rpow 3 ((1 + s) * ↑(n - 2)) * Gsem)))) : Exc (n - ↑k) ≤ thetaK * Exc n + stepFourEpsCoeff Crem Vd C s (ExcessDecay.endpointConst d (1 / 9)) * epsj * Slp n + stepFourDeltaOut Crem Vd C s epsj 0 (s ^ (-(5 / 2)) * SigInvN2) Kg 0 n

The Step-4 collapse on the interior branch, over abstract reals: the two-leg display becomes hstep4's body at the unshifted ratio θ^k.

3. The two per-leg re-pins

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourGsemLeg_shift_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {z : HCPolySupport.Vec d} {m n : ℤ} {g : HCPolySupport.Vec d → E} {K s : ℝ} (hd : 1 ≤ d) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K g) : (Support.normalizedGagliardoESeminormOn (stepThreeWindow z m n) s g).toReal ≤ K * stepFourGagliardoConst d s * 3 ^ (↑(n + 1) * (1 / 2 - s))

The one-scale re-pin of the Gagliardo exponent.'s comparison is read at the interior clause's OWN window index n, and moved to the collapse's n+1 for free, because 1/2 - s > 0.

theorem Algsuperdiff.Section4.Provider.Regularity.sigmaBar_shift_weighted {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) (hgamma : M.gamma ≤ 1 / 4) {n : ℤ} (hn : n ≤ m0) {s : ℝ} (hs : 0 < s) : s ^ (-(5 / 2)) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ ≤ 8 * (s ^ (-(5 / 2)) * (↑(Section3.Annealed.sigmaBar M n))⁻¹)