ShiftedG1Lane #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The 𝒢₁ proportion lane re-based at an arbitrary scale m₀ #
Every proved §4.1 proportion lane averages over the window {0,…,n} (the
Finset.Icc (0:ℤ) (n:ℤ) inside IndicatorDensity.scaleProp), while the
proportion display of the manuscript quantifies over the scales m₀ + k. The
generic transport is carried out once, in ShiftedConcentration
(ratioTail_of_concentration_shift); this module runs the two 𝒢₁ lanes
through it, so that the 𝒢₁ proportion tail is available at every base scale.
Contents #
ratioTail_of_shellArray_shift— the single-shell array engine at basem₀. Same hypothesis list as the base-0shell-array engine, except that the deterministic reduction is asked at everym : ℤ(the base-0form asks it only atm ≥ 0, and the sign binder is unused in both𝒢₁lanes).hreduce_eventG1a_all,hreduce_eventG1b_all— the two lane reductions without the0 ≤ mbinder, so that they can be instantiated at a negative scale. Nothing else changes: both go through the public, sign-condition-freelt_Yk_of_lt_rowGE.ratioTail_eventG1a_shift,ratioTail_eventG1b_shift— the two lanes at basem₀. The null enlargement is unchanged: the enlarged shifted family is the shift of the enlarged family.ratioTail_eventG1_of_lanes_shift,ratioTail_eventG1_shift— the½θrecombination and the composed tail, both at basem₀.ratioTail_eventG1_of_majorant_shift,ratioTail_eventG1_shellThreshold_shift— the same explicit parameter package as theG1ThresholdArithmajorant, re-run at basem₀.
Why the parameter arithmetic is re-elaborated here #
The base-0 majorant route builds its parameter package (Lam, U, V, p,
p₂, D, D₂, the two rate conditions, the two threshold conditions) inside
a closed proof and exposes none of it, and the arithmetic helpers it consumes
are private to that module. The package is index-free —
it never mentions the window, the base scale, or the family — so the honest
route at base m₀ is to re-elaborate the very same arithmetic and change only
the final application. That is what is done below.
References #
- ABK26,
l.ratio.of.good.scales.for.k. - ABK26,
p.concentration.for.scales, (them₀reduction). - ABK26,
d.good.event.for.lambda.
1. The single-shell array engine at base m₀ #
The proportion tail of one 𝒢₁ lane over the window {m₀,…,m₀+n}.
The hypothesis list is that of the base-0 shell-array engine, with the
deterministic reduction asked at every scale m : ℤ and the base scale m₀
inserted before the window length. Both Appendix-D hypotheses are discharged
inside exactly as in the base-0 engine; the endpoint is the re-based
ratioTail_of_concentration_shift, which transports the concentration
proposition by the diagonal translation of the array.
2. The two lane reductions, without the unused sign binder #
The hreduce slot of the large-waves lane, at every scale.
The large-waves reduction without a sign binder on m, which costs nothing:
lt_Yk_of_lt_rowGE and lt_rowGE_of_notMem_eventG1a are both stated at an
arbitrary scale. The re-based engine instantiates the reduction at negative
scales.
The hreduce slot of the small-waves lane, at every scale.
The small-waves reduction without a sign binder on m, which costs nothing:
lt_Yk_of_lt_rowGE and lt_rowGE_of_notMem_eventG1b are both stated at an
arbitrary scale.
3. The two lanes at base m₀ #
The large-waves proportion tail over the window {m₀,…,m₀+n}, with the
hypothesis list of the base-0 large-waves lane.
The small-waves proportion tail over the window {m₀,…,m₀+n}, with the
hypothesis list of the base-0 small-waves lane.
4. The ½θ recombination and the composed tail at base m₀ #
The ½θ recombination of the two 𝒢₁ lanes over {m₀,…,m₀+n}. The
inclusion is the generic setOf_scaleProp_inter_subset, and the identification
of 𝒢₁ with the intersection of the two named conditions holds at every
scale, hence in particular at m₀ + k.
The 𝒢₁ proportion tail over the window {m₀,…,m₀+n}, with the hypothesis
list of the base-0 𝒢₁ tail: the two moment exponents, the two
Appendix-D normalizers, the two rate conditions and the two threshold
conditions.
5. Abstract-real helpers for the parameter arithmetic #
These are the arithmetic helpers of the proved G1ThresholdArith route,
re-elaborated here because the originals are private to that module. Every
transcendental atom (Real.exp, Real.log, Real.rpow, Real.sqrt) is
confined to this section.
6. The 𝒢₁ proportion tail at the explicit majorant, at base m₀ #
The 𝒢₁ proportion tail above the explicit majorant, over the window
{m₀,…,m₀+n}.
The parameter package is exactly the one the base-0 majorant route builds:
the moment exponents p = 64 r Λ/θ + 2
and p₂ = 256 r Λ/(sθ) + 8/s + 1 with Λ = log(6r) + c₁ r, the two Γ-moment
normalisers, the two rate conditions, and the two threshold conditions. None
of it mentions the window or the base scale, so the only difference from the
base-0 route is the final application, which is the re-based
ratioTail_eventG1_shift.
7. The 𝒢₁ proportion tail at the frozen support threshold, at base m₀ #
The 𝒢₁ proportion tail at the support threshold, over the window
{m₀,…,m₀+n}. Under the explicit parameter condition hcond, the 𝒢₁
bad-scale density at the threshold s ε √(c⋆) (√γ)⁻¹ obeys the exp(-c₁n)/3
tail at every base scale m₀. The threshold comparison is the proved, already
index-free g1Majorant_le_shellThreshold.