AtomTail #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-atom Γ_{1/3} tail of the 𝒢₀ bracket #
ABK26, §4.1, l.good.scales.ratio.lambda, the per-annulus atom tail, display:
( σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; 𝐚_{k−2}) − C_{(e.cg.ellip.lower)} )_+
≤ 𝒪_{Γ_{1/3}} ( exp( − C^{−1} c⋆² γ^{−1} ) ) , k ∈ ℤ.
The left side is Localize.cgExcess M Ccg (k−2) z at the definite
constant Support.cgEllipLowerConstant d (the same choice the frozen 𝒢₀
uses, so no cross-anchor witness mismatch is possible). The right side is
produced here from the Section 3 anchor
Frozen.Section3.coarse_ellipticity_bounds alone.
What the anchor gives, and how it is instantiated #
The anchor's lower leg is a Probability.IsLowerIntegerFamilyOrlicz: ONE
measurable witness Y with
∀ ω, ∀ L ≥ m−1, λ_{s,q}^{-1}(□_m; 𝐚_L)(ω) · σ_{m−1} ≤ b + Y ω, andY ≤ 𝒪_{Γ_{(1−σ)/2}}(exp(−(C_cg^{−1} E^{−2} γ^{−1}))),
for b = lowerEllipticityProfile C_cg γ s q. The instantiation used here is
| anchor slot | value | why |
|---|---|---|
m | k − 2 | the 𝒢₀ bracket's cube index; then m − 1 = k − 3 is its σ index |
L | k − 2 | the 𝒢₀ bracket's truncation index; k − 2 ≥ k − 3 |
σ | 1/3 | Γ_{(1−σ)/2} = Γ_{1/3} is the tex's index (graph) |
q | Support.coarseEllipticityExponentTwo | 𝒢₀ reads λ_{γ,2}^{-1} |
s | M.gamma | 𝒢₀ reads λ_{γ,2}^{-1} |
At s = γ and q = 2 the deterministic shift collapses to the bare constant,
lowerEllipticityProfile C_cg γ γ 2 = C_cg γ (2γ−γ)^{−1} = C_cg
(lowerEllipticityProfile_two_diag), which is why the manuscript's
C_{(e.cg.ellip.lower)} is a pure constant and why the bracket subtracted
inside 𝒢₀ is exactly the anchor's own shift.
The lattice z: stationarity, not a new estimate #
The 𝒢₀ bracket at the lattice centre z is the origin bracket read at the
translated sample. The tail therefore transfers by the law-level
stationarity GoodEvents.measurePreserving_translateCutoffSample (valid for
real z), through the generic device isBigOWith_comp_measurePreserving
proved below. No per-z instance of the anchor is used, and no lattice
restriction is needed.
References #
- ABK26,
l.good.scales.ratio.lambda, statement, proof; the atom-tail step. p.cg.ellipticity.bounds=Frozen.Section3.coarse_ellipticity_bounds.
1. Two generic weak-Orlicz devices #
A weak-Orlicz upper tail transports along a measure-preserving map. The
tail event of X ∘ T is the T-preimage of the tail event of X, and a
measure-preserving map does not change its mass. This is the device that turns
the origin-centred estimate into the estimate at an arbitrary lattice centre.
Clamping at zero does not change a weak-Orlicz upper tail at a positive
scale. For A > 0 and t ≥ 1 the level A t is positive, so the tail events
of X and of max X 0 coincide. This is what turns the anchor's witness Y
into a bound for the positive part (·)_+.
2. The deterministic shift at the diagonal window s = γ, q = 2 #
lowerEllipticityProfile C γ γ 2 = C. The anchor's deterministic shift at
the 𝒢₀ parameters is the bare constant: the pole s (2s − γ)^{−1} equals 1
on the diagonal s = γ. This is the identification that lets the 𝒢₀ bracket
subtract the anchor's own shift and call it C_{(e.cg.ellip.lower)}.
3. The Orlicz amplitude #
The amplitude of the coarse-ellipticity display, exp(−(C_cg^{−1} E^{−2} γ^{−1})). At the budget E = C c⋆^{−1} supplied this is exp(−(C_cg C²)^{−1} c⋆² γ^{−1}), the manuscript's exp(−C^{−1} c⋆² γ^{−1}).
Equations
Instances For
4. The per-atom tail #
The 𝒢₀ atom tail, at the anchor's own premises.
( σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; 𝐚_{k−2}) − C_{(e.cg.ellip.lower)} )_+
≤ 𝒪_{Γ_{1/3}} ( exp(−(C_cg^{−1} E^{−2} γ^{−1})) )
for k ∈ ℤ real centre z (in particular every triadic lattice point). The
constant subtracted is Support.cgEllipLowerConstant d, the same definite
choice the frozen 𝒢₀ uses.
The hypotheses are exactly the anchor's, at σ = 1/3, s = γ, q = 2:
hstate is 𝒮(k−3, E), hE and hEup are its E-window, and hwin is its
s-window read at s = γ.
5. The packaged form, through's all-scales budget #
The 𝒢₀ atom tail in the printed shape.
There is a dimensional constant C(d) such that every model in the printed
regime γ ≤ C^{−10} c⋆^{10} — and satisfying the anchor's own s-window at s = γ — has, for every k ∈ ℤ and every real centre z,
( σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; 𝐚_{k−2}) − C_{(e.cg.ellip.lower)} )_+
≤ 𝒪_{Γ_{1/3}} ( exp(−(C_cg C²)^{−1} c⋆² γ^{−1}) ) ,
the amplitude being the manuscript's exp(−C^{−1} c⋆² γ^{−1}) after the
E = C c⋆^{−1} substitution E^{−2} = C^{−2} c⋆².
The induction state and both E-window premises of p.cg.ellipticity.bounds
are discharged here, by exists_allScalesInductionState_ge at the floor
(3/2)·exp(3 C_cg) and the proved c⋆ ≤ 3/2. The s-window premise hwin is passed
through: it is the anchor's own window and is a caller obligation.