HsepReduction #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The 3^{gamma hsep} reduction: the Orlicz half #
Step 3 of p.bfA.multiscalebound (ABK26) reduces the prefactor 3^{gamma hsep} to 2 + (something of size exp(-c gamma^{-1})).
3^{gamma hsep} <= 1 + 3 gamma hsep 1_{gamma hsep <= 3^{-4}}
+ 3^{gamma hsep} 1_{gamma hsep > 3^{-4}}
<= 2 + 3^{gamma hsep} 1_{gamma hsep > 3^{-4}}
<= 2 + O_{Gamma_4}(1) . O_{Gamma_4}(exp(-c gamma^{-1})) .
The deterministic half is proved:
ConclusionArithmetic.three_rpow_le_two_add_indicator. This module proves the
Orlicz half, i.e. the last line, at explicit exponents and an explicit
scale, out of the three ingredients names:
e.hsep.tailsfor theO(1)factor, at the proved amplitude (Percolation.isBigOWith_gammaSigma_three_rpow_hsep_of_gates, which controls3^{b hsep}atGamma_{1-sigma}); the passage from3^{gamma hsep}to3^{b hsep}is's owngamma <= bstep, proved asConclusionAssembly.three_rpow_gamma_hsep_le_three_rpow_b_hsep;e.indc.O.sigmafor the indicator (WaveOscillationsCore.isBigOWith_gammaSigma_indicator_natLtat the event{i < hsep}), applied at the integer thresholdi = floor((81 gamma)^{-1}), which is exactly the discretization of{gamma hsep > 3^{-4}}:'s own computationP[gamma hsep > 3^{-4}] <= exp(-exp(3^{-4} b gamma^{-1}))is this event's tail, and the resulting scale(K 3^{-b floor((81 gamma)^{-1})})^{(1-sigma)/sigma_2}is the advertisedexp(-c gamma^{-1})size;e.multGammasigfor the product (Orlicz.ProductPower.isBigOWith_gammaSigma_mul_of_nonneg, carrying CoarseGraining's explicitgammaProductConst).
Exponent bookkeeping #
prints Gamma_4 on both factors and on the product. At this repository's
proved amplitude index the input is Gamma_{1-sigma} with sigma > 0, i.e.
sigma_1 < 1, so what is proved is
Gamma_tau , tau = (1-sigma) sigma_2 / ((1-sigma) + sigma_2)
on the product. sigma_2 > 0 is free, so tau can be made any value below `1
- sigma
; the manuscript's "upon relabellingsigma" is exactly this freedom. NeitherGamma_4norGamma_2is attainable from aGamma_{1-sigma}input withsigma > 0`; nothing below claims either.
What is not proved #
The final numerical comparison "(K 3^{-b floor((81 gamma)^{-1})})^{(1-sigma)/sigma_2} <= C exp(-c gamma^{-1})" is not proved: the
scale is carried in the exact closed form above, which is stronger than any
exp(-c gamma^{-1}) claim and avoids inventing a c. A consumer that wants
the printed shape can bound floor((81 gamma)^{-1}) >= (81 gamma)^{-1} - 1.
References #
- ABK26,
p.bfA.multiscalebound, Step 3;e.hsep.tails;e.indc.O.sigma;e.multGammasig.
Monotonicity of the weak-Orlicz bound #
A pointwise-smaller variable inherits the Gamma_sigma bound at the same
scale: the upper-tail events are nested. (CoarseGraining carries mono_scale;
this is the missing mono in the function argument.)
The O(1) factor: 3^{gamma hsep} at Gamma_{1-sigma} #
e.hsep.tails read at the Step-3 prefactor ('s O_{Gamma_4}(1) factor).
Under gamma <= b, the prefactor 3^{gamma hsep} inherits the proved
Gamma_{1-sigma} bound of 3^{b hsep} at the same amplitude.
The indicator factor: e.indc.O.sigma at the threshold #
The threshold event, discretized: gamma hsep > 3^{-4} forces hsep > (81 gamma)^{-1}, hence floor((81 gamma)^{-1}) < hsep.
e.indc.O.sigma's indicator. The indicator `1_{gamma hsep
3^{-4}}
isO_{Gamma_{sigma_2}}` at the scale
(K 3^{-b floor((81 gamma)^{-1})})^{(1-sigma)/sigma_2} ,
K = hsepAmplitude sigma b ,
which is's own exp(-c gamma^{-1}) size (the exponent is linear in
gamma^{-1}). The free exponent sigma_2 > 0 is e.indc.O.sigma's own t = 1/sigma_2.
The product: e.multGammasig #
The Orlicz half's display. The random summand's corrected inequality is
Gamma_tau with tau = (1-sigma) sigma_2/((1-sigma) + sigma_2) at the explicit
scale
gammaProductConst (1-sigma) sigma_2 . hsepAmplitude sigma b
. (hsepAmplitude sigma b . 3^{-b floor((81 gamma)^{-1})})^{(1-sigma)/sigma_2} .
The Step 3 display, both halves. Pointwise the prefactor is <= 2 + Z,
and Z is Gamma_tau at the explicit exp(-c gamma^{-1})-sized scale:
3^{gamma hsep} <= 2 + 3^{gamma hsep} 1_{gamma hsep > 3^{-4}} ,
3^{gamma hsep} 1_{gamma hsep > 3^{-4}}
<= O_{Gamma_tau}( C . K . (K 3^{-b floor((81 gamma)^{-1})})^{(1-sigma)/sigma_2} ) .
The first line is ConclusionArithmetic.three_rpow_le_two_add_indicator
(ABK26's own deterministic split, at 3 . 3^{-4} < 1); the second is
isBigOWith_gammaSigma_three_rpow_gamma_hsep_mul_indicator. Together they are
exactly the corrected display of ABK26, with the printed O_{Gamma_4}(exp(-c gamma^{-1})) summand of the right-hand side removed as ABK26 requires.