LambdaIndexUpscale #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Bullet (B5) at the indices: the domain/field upscaling for λ^{-1} #
The index gap this module closes #
LambdaSlotB5.lean delivers bullet (B5) at the anchor's own matched triple
(□_{k−2}, 𝐚_{k−2}, σ_{k−3}). Read in the Step-4 indices this is the cube
□_j with the field 𝐚_j, whereas the printed bullet carries the field
𝐚_{j−2} at the same cube □_j and the same gauge σ_{j−1}.
The route, and every constant it costs #
Read the delivered atom at the lower index k = j, i.e. at the triple (□_{j−2}, 𝐚_{j−2}, σ_{j−3}), and raise the domain back to □_j:
- The domain raise.
lambdaSq_finite_two_inv_le_nine_pow_mul_max_descendants_sub_two(Annular/LambdaMatrixRoute.lean) givesλ_{γ,2}^{-1}(□_j;𝐚_{j−2}) ≤ (1 + 9^d 3^{−4γ}) max_R λ_{γ,2}^{-1}(R;𝐚_{j−2})over the9^dscale-(j−2)descendantsRof□_j, at the SAME gauge and the SAME field. The sharp constant is only relaxed to1 + 9^d. - The atom tail at every descendant. Each descendant is the cube
3^{j−2}w + □_{j−2}at the field𝐚_{j−2}, i.e. exactly the delivered atom atk = jand the real centre3^{j−2}w; the provedProportion.exists_cgExcess_atomTailholds real centre, andLambdaWindow.exists_cgExcess_atomTail_unconditionalremoves its window. - The Orlicz finite maximum.
Orlicz.isBigOWith_gammaSigma_finset_sup'_of_nonemptyatσ = 1/3converts the9^dindividualΓ_{1/3}tails into one tail for their maximum, at the common amplitude times(3 max{1, log 9^d})^{3}(theq^{1/σ}normalization atσ = 1/3), ad-only factor. - W3's index steps, twice.
Annular.sigmaBar_sub_two_le_eight_mul_sigmaBar_sub_threegivesσ_{j−1} ≤ 8 σ_{j−2} ≤ 64 σ_{j−3}, i.e.σ_{j−3}^{-1} ≤ 64 σ_{j−1}^{-1}, which is what turns the delivered gauge into the printed one.
Net deterministic constant 64(1 + 9^d), d-only; the Orlicz leg carries in
addition the d-only maximum factor of step 3. No γ-exponent and no
s-power is moved anywhere in this module: the gauge stays γ, the exponent
stays q = 2, and the amplitude stays the exp(−C_cg^{−1}E^{−2}γ^{−1}).
References #
- ABK26,
l.bounds.mathcal.E.aLbullet (B5);p.cg.ellipticity.bounds.
1. Three local re-derivations #
2. The printed atom and its descendant family #
The (B5) left-hand side, λ_{γ,2}^{-1}(z + □_j; 𝐚_{j−2}): domain scale
j, cutoff scale j − 2, gauge γ, exponent q = 2, with the cube translate
realized on the sample (resolution A4). At z = 0 this is the manuscript's
centred λ_{γ,2}^{-1}(□_j; 𝐚_{j−2}) verbatim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 9^d scale-(j−2) descendants of □_j are never empty.
Their number is exactly 9^d.
The 𝒢₀ bracket, maximized over the 9^d descendants of z + □_j.
This is the single random variable the Orlicz finite-maximum estimate produces,
and the one that carries the whole Γ_{1/3} tail of the upscaled bullet.
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The pointwise upscaling (state-free) #
A7's domain raise, read at the 𝒢₀ bracket.
λ_{γ,2}^{-1}(z+□_j;𝐚_{j−2}) ≤ (1+9^d)(σ_{j−3}^{-1}C_cg + σ_{j−3}^{-1}𝒳^{max}),
where 𝒳^{max} is the maximum of the 𝒢₀ brackets over the 9^d scale-(j−2)
descendants. No induction state and no probability enters: this is the
deterministic half of the upscaling.
4. W3's two index steps #
σ_{j−3}^{-1} ≤ 64 σ_{j−1}^{-1} — two applications of the one-step
running-diffusivity ratio σ_{n−2} ≤ 8 σ_{n−3}. This is what converts the
delivered gauge σ_{j−3} into the printed σ_{j−1}.
5. The upscaled bullet, at the printed indices #
The d-only Orlicz factor of the finite maximum over the 9^d
descendants, (3 max{1, log 9^d})^{1/σ} at σ = 1/3.
Equations
Instances For
The Γ_{1/3} tail of the descendant maximum.
Bullet (B5) at the printed indices, at every moment q ∈ [1,∞).
E[ λ_{γ,2}^{-q}(z + □_j; 𝐚_{j−2}) ]^{1/q}
≤ 64(1+9^d) σ_{j−1}^{-1} C_cg
+ C(1/3) q³ · 64(1+9^d)(3 max{1,log 9^d})³ σ_{j−1}^{-1} exp(−C_cg^{−1}E^{−2}γ^{−1}) ,
The q³ is q^{1/σ} at σ = 1/3. Every constant is d-only.
The upscaled bullet, packaged and unconditional in the printed regime.
There is a d-only constant C such that every model with γ ≤ C^{−10}c⋆^{10} satisfies bullet (B5) at the printed cube, field and gauge, at
every scale j, every real centre z and every moment q ∈ [1,∞), with NO
remaining hypothesis: the induction state comes from its all-scales budget and the
s-window from LambdaWindow.cgTailScale_le_half_gamma.