MajorantSlots #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two L-carrying slots of Step 3's display, and the L-free majorant #
Nothing here imports that file, and nothing here claims the anchor.
The mechanism #
Step3BlockSplit.step3Display is a function of the truncation index L only
through the two unit-cube gauges of the recentered shell
h = k_L − k_{j−2} − (k_L − k_m)_{□_m}:
(step3Shell M L m R hle ω).gradientW1Infinity and (step3Shell M L m R hle ω).valueL2 .
Every other ingredient -- σ_m, σ_{j−2}, unitCubeLambda (2γ) and
unitCubeHomogenizationError at unitRescaledCutoffCoeff M R (R.scale − 2) ω
-- is built from the cutoff at level R.scale − 2 and is L-free. This module
makes that structural fact usable:
step3DisplayAtis Step 3's display with the two gauges replaced by abstract real slots;step3Display_eq_step3DisplayAtis therflidentification;step3DisplayAt_monois the monotonicity of the display in both slots, which is what converts upper bounds on the two gauges into an upper bound on the display. Its abstract-real core keeps the twoReal.rpowatoms opaque.
Consequently, any pair of L-free upper bounds for the two gauges produces an
L-free majorant of step3Display, and hence -- through
Step3BlockSplit.exists_normalizedBlockResponseMax_step3_split, which needs the
display at ω and at the negated sample Nω -- an L-free majorant of the
Step-1 endpoint's per-cube block response maximum. That majorant is
lFreeStep3Majorant.
The two slot bounds themselves (the geometric shell-sum route) are the business
of ShellSlotBounds.lean; the composition with the expectation transport is
MajorantTransport.lean.
What is a hypothesis here, and why #
step3DisplayAt_mono needs the sign facts 0 ≤ C, 0 < σ, 0 ≤ λ^{-1},
0 ≤ grad, 0 ≤ val and the nonnegativity of the two printed exponents
2s/(1−4γ), 4γ/(1−4γ); the last is where γ ≤ 1/8 is used, exactly the
binder Step3BlockSplit already carries. The slot bounds GB, VB are
parameters: they are supplied by the caller and are not source premises.
References #
- ABK26,
l.bounds.mathcal.E.aL, (Step 3).
Step 3's display with abstract gauge slots #
Step 3's display, with the two L-carrying gauges abstracted.
step3Display L m R hle ω s is this expression at grad = (step3Shell M L m R hle ω).gradientW1Infinity and val = (step3Shell M L m R hle ω).valueL2;
nothing else in it mentions L.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The slot identification. Step 3's display IS step3DisplayAt at the two
gauges of the recentered shell; the L-dependence of the left-hand side lives
entirely in those two slots.
Monotonicity in the two slots #
The display is monotone in both gauge slots.
Enlarging the gradient gauge and the L² gauge enlarges Step 3's display: the
first slot occurs in the two (1 + grad λ^{-1})-powers (nonnegative exponents)
and in the last square, the second slot only through val².
The L-free majorant #
The L-free majorant of the Step-1 endpoint's per-cube object.
Given L-free upper bounds GB R ω, VB R ω for the two gauges of the
recentered shell at the cube R, this is Step 3's display at those bounds, read
at ω and at the negated sample Nω -- the two legs of the primal/adjoint
split of Step3BlockSplit.exists_normalizedBlockResponseMax_step3_split.
It does not mention L.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two-sample display sum is dominated by the L-free majorant.
The hypotheses are the two slot bounds at the two samples the split needs (ω
and Nω), each uniformly in L ≥ m; the conclusion is L-free. This is the
step that removes L from Step 3's display. The slot bounds are required at
these two samples ONLY, which is what lets a caller supply them almost surely.