StepFourCollapseInterface #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity Step 4: the collapse of the excess-decay one-step into hstep4 #
What this module is #
StepFiveIterationResult.iterationDecay_of_stepFourDecay takes ONE
mathematical input, hstep4:
∀ j, n + k ≤ j → j ≤ m - 1 → j ∉ 𝓑_z →
E(u, U_{j-k}) ≤ θ^k E(u, U_j) + ε_j |∇ℓ_j| + δ_j .
The excess-decay lane's anchored interior one-step delivers, at each scale n,
a display of the shape
E(u, U_{n-k}) ≤ C_con E(u, U_n)
+ C_rem · 3^{-n} · √((3²)^d) · ( T₁ + T₂ + T₃ + T₄ ) ,
T₁ = C s^{-4} 𝓔_{n+1} ( ‖u-(u)‖_{L²(U_{n+1})} + s^{-3/2} 3^{n-2} |(∇h)_{U_n}| ) ,
T₂ = C s^{-7} σ_{n-2}^{-1} 3^{(1+s)(n-2)} [g]_{H^s(U_{n+1})} ,
T₃ = C s^{-6} 3^{(1+s)(n-2)} [∇h]_{H^s(U_{n+1})} ,
T₄ = C s^{-6} 3^{n-2} ‖∇h‖_{L²(U_{n+1})} .
Every conversion is named and separately proved:
edLeg_one_le— the𝓔-leg fold. Its oscillation half is absorbed into the contraction (this is the term prices; seeStepFourCollapseWeights), its slope half IS theε_j |∇ℓ_j|leg, and its datum half iss^{-3/2}·(1/9)·‖∇h‖_∞(weightthree_weight_flat).edLeg_three_le— the∇hseminorm leg, same collapse, noσ.edLeg_four_le— theL²-datum leg, weight1/9.
The three mismatches, carried rather than absorbed #
- The
ε-slot carries a coefficient. The producedεisstepFourEpsCoeff · ε_jwithstepFourEpsCoeff = C_rem V_d C s^{-4} C_osc, NOT the rawε_jat whichStepFiveIterationResult'se.sum.eps.j.boundslot is pinned (constant2). - The gate scale shifts by one — see
StepFourCollapseEps; the producedεreadsε_{j+1}. δ_n's∇hlegs are ungated, and one of them does not decay. The Step-5 family multiplies its∇hlegs by1_{z ∉ □_{m-1}}and its seminorm legs are[·]_{W^{1/2,∞}(□_m)}, whereas the excess-decay display carries them at everyzand produces them at the Hölder constantsK_h,K_{h,∞}(which DOMINATE those seminorms); moreoverT₄collapses to the flatC s^{-6}·(1/9)·‖∇h‖_∞, with no decay inn, so its window sum is(m-n+1)-linear rather than2δ(m-n)-linear. The producedδhere is thereforestepFourDeltaOut, which is larger than the Step-5 family; feeding the Step-5 concrete endpoint at its own pinned family is not available from this display.
The abstract excess-decay leg interface #
The display above enters here as the hypothesis hed of
stepFourDecay_of_edOneStep, with the four leg values abstract reals and the
scale weights, the 3^{-n} normalizer and the nesting written exactly as the
excess-decay lane's anchored interior one-step writes them. The final stitch
is therefore one application: instantiate
Exc j := affineExcess (truncatedWindow z m j) u , Slp j := slopeMagnitude (g j) ,
Ccon := taylorContractionConst d * schauderWindowConst d * windowRatioConst d 2
* (3^{-k})^{1/2} ,
Crem := triangleRemainderConst d (schauderWindowConst d) k ,
Vd := √((3²)^d) , Efl := fluxCorrectedErrorRepresentative … ,
and the six leg values at the display's own terms.
References #
- ABK26,
t.regularityStep 4;l.excess.decay.good.scales.
1. The four leg conversions #
The 𝓔-leg conversion. T₁'s oscillation half folds into C_osc (E + |∇ℓ|) (the hypothesis hOsc residue (2)) and its datum half collapses at the
flat weight 3^{-n} 3^{n-2} = 1/9.
The g-leg conversion: the shom-weight conversion in place. The
excess-decay leg's σ_{n-2}^{-1} becomes the Step-5 slot's σ_n^{-1} at the
absolute constant 8, and the three scale factors collapse to 3^{n/2}.
2. The produced ε-coefficient and δ_n #
The coefficient the collapse puts on ε_j. Measured mismatch (1): the
Step-5 ε-slot is pinned at the ε_j, this is C_rem V_d C s^{-4} C_osc
times it.
Equations
Instances For
The δ_n the collapse produces, in the Step-5 slot's own weights: the
g-leg at 3^{n/2} σ_n^{-1} K_g (constant 8 from the shom-weight
conversion), the ∇h seminorm leg at 3^{n/2} K_h, and the two flat datum
legs. Larger than the Step-5 family — measured mismatch (3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bracket bound: the whole excess-decay remainder, split into the
absorbable contraction (C_ε ε_j) E, the ε_j |∇ℓ| leg, and δ_n.
3. The endpoint: hstep4's body at one scale #
The Step-4 collapse. The excess-decay lane's one-step display (hed,
written exactly as the lane's anchored interior one-step writes it, with the six
leg values abstract) becomes the body of
StepFiveIterationResult.iterationDecay_of_stepFourDecay's hstep4 at the
scale n:
E_{n-k} ≤ θ^k E_n + (C_ε ε_j) |∇ℓ_n| + δ_n .
The Step-4 g-comparison in the toReal shape the leg conversions consume: on
the Step-3 window U_j = (z+□_j) ∩ □_m, at any index 0 < s < 1/2,
[g]_{H^s(U_j)} ≤ ( K · C_{S4.4}(d,s) ) · 3^{j(1/2-s)} ,
K the C^{0,1/2}(□_m) bound of g. Instantiated at the excess-decay leg's
own window index j := n+1 this is exactly edLeg_two_le's /
edLeg_three_le's hypothesis hGsem / hHsem, at K_g := K · C_{S4.4}(d,s).