ValueSlotLinfty #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
B6, second half: the L∞ leg of the L-free value slot #
What this module does #
ShellSlotBounds.lFreeValueSlot has two summands.
‖k_m − k_{j−2}‖_{L∞(3^j v + □_j)}
= Cutoff.localCubeControl j (translate (3^j v) (shellIncrement ω (j−2) m)) .
It is settled here by ONE application of the proved covering-plus-maximum
machinery of Stream/LargeCubeLinfty.lean (ABK26's e.km.kn.Linfty), read at
the index triple (n, m, l) = (j−2, m, j) and at the translated centre 3^j v: the cube 3^j v + □_j is covered by (2·3^{3} + 1)^d translates of cubes
of scale j − 2, on each of which the proved small-cube bound
Stream.translatedIncrementSupBound applies at the SAME amplitude as at the
origin (one-shell stationarity, TranslatedTransport.lean). Because l − n = 2, the maximum lemma's (log N)^{1/2} factor is a pure d-constant.
The covering family, the rounding argument and the count are the proved
subcubeShifts/exists_subcubeShift_mem/three_mul_max_one_log_card_subcubeShifts_le;
only the base point is new, and it is a silent parameter throughout
(translatedLargeCubeSupBound below is the proved largeCubeSupBound with
each covering centre shifted by z).
The honest display, and how it differs from the printed one #
The proved amplitude at (n, m) = (j−2, m) carries min{γ^{-1/2}, (m − j + 2)^{1/2}}, NOT the printed min{γ^{-1/2}, (m−j)^{1/2}}. The two differ only
by a constant when j ≤ m − 1, but at the endpoint j = m the printed minimum
is 0 while the left-hand side contains the nondegenerate block k_m − k_{m−2}. The display proved here is therefore
‖k_m − k_{j−2}‖_{L∞(3^j v + □_j)}
= 𝒪_{Γ₂}( C(d) ( 1 + min{γ^{-1/2}, (m−j)^{1/2}} ) 3^{γ m} ) ,
with the additive 1 that the endpoint forces.
References #
- ABK26, (
e.km.kn.Linfty), (e.km.kn.Linfty.smallcube), (e.k.ell.upscales.infty), (bullet (B6), second half).
1. The covering maximum at a translated centre #
The proved covering maximum of Stream/LargeCubeLinfty.lean with every
covering centre shifted by z: the single random variable dominating ‖k_m − k_n‖_{L∞(z + □_l)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deterministic half at a translated centre. At every point of
z + □_l the finite stream increment is dominated by the covering maximum.
The probabilistic half at a translated centre, at the amplitude of the
proved centred display: each member of the shifted cover is itself a translated
small cube, so isBigOWith_gammaSigma_translatedIncrementSupBound prices it.
2. The deterministic bridge to the value gauge of the slot #
The translated increment shell field evaluates to the finite stream increment at the translated point.
The value gauge of the translated increment is dominated by the covering
maximum. This is e.km.kn.Linfty's deterministic half in the exact carrier
shape used by ShellSlotBounds.lFreeValueSlot.
3. The amplitude arithmetic #
Local re-derivation of a private helper of
Stream/LargeCubeW1Inf.lean.
The endpoint-safe comparison of the two minima. The covering route
reads the increment from the scale n = j − 2, so its (m − n)^{1/2} leg is
(t + 2)^{1/2} where t = m − j. On the integer range t ∈ {0} ∪ [1, ∞) this
is at most twice 1 + min{a, t^{1/2}} -- the additive 1 is exactly what the
endpoint t = 0 forces.
The explicit dimensional constant of the L∞ leg.
Equations
Instances For
4. The Γ₂ display of the L∞ leg #
‖k_m − k_{j−2}‖_{L∞(3^j v + □_j)} = 𝒪_{Γ₂}(C(d)(1 + min{γ^{-1/2},(m−j)^{1/2}})3^{γm}).
The additive 1 is forced at j = m, where the printed minimum vanishes while
the left-hand side contains the nondegenerate block k_m − k_{m−2}; for j ≤ m − 1 the minimum is at least 1 and the display is the printed one up to the
constant.