G2SharpArith #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The 𝒢₂ ε-threshold at the LOG-QUANTILE reading of θ^{-1/p} #
What changes, and why #
RatioTailArith.threshold_le_inv — the step that puts Appendix D's threshold
9 s'^{-1} C⋆^{1/p} θ^{-1/p} below the row normalizer's reciprocal — pays the
quantile factor θ^{-1/p} by the crude bound θ^{-1/p} ≤ θ^{-1}. That single
step is where a whole polynomial power of 1/θ enters the 𝒢₂ threshold: it is
the reason the crude reading of that threshold carries the divisor θ and the
reason its binding clause carries θ² rather than θ.
The honest reading is logarithmic: θ^{-1/p} ≤ 3 as soon as
log(1/θ) ≤ p log 3, and log(1/θ) ≤ 1/θ − 1, so the existing moment exponent
already pays for it — g2MomentExponent's rate branch is at least 64/θ, which
dominates 1/θ. No new branch, no new hypothesis, no new parameter: the
quantile power of 1/θ is simply not there.
Contents #
rpow_neg_inv_le_three—θ^{-1/p} ≤ 3fromθ⁻¹ ≤ p(the log-quantile step);threshold_le_inv_sharp— the sharp twin ofRatioTailArith.threshold_le_inv, at theθ-free key condition27 D (1+C⋆) ≤ s';inv_theta_le_g2MomentExponent— the proved moment exponent already exceedsθ⁻¹, so the sharp step is available with the lane's ownp;g2ThresholdSharp d r s θ c₁ = 108(1+C⋆)·D— theθ-freeε²-threshold (contrastg2Threshold … = 36(1+C⋆)·D/θ);g2ThresholdSharp_le_ofandg2ThresholdSharp_le_of_gammaPow— the sufficient parameter conditions, in two clauses.
The two sharp clauses #
Writing κ₁(d), κ₂(d) for G2ThresholdArith.g2ThresholdConstOne/Two:
(1) 3κ₁(d) r² (1+c₁) C² γ ≤ θ c⋆² s⁵ ε²
(2) 3κ₂(d) r⁸ (1+c₁)⁴ exp(−2c⋆³/(Cγ)) ≤ θ⁴ s⁹ ε²
Each is the corresponding clause of the crude reading with one power of θ
removed from the right-hand side and the constant tripled.
That single power of θ is the whole content of the sharpening: against the
consumer's own coupling ε² = s²θ, clause (1) reads γ ≲ θ², i.e. θ ≳ γ^{1/2} — the printed Theorem-C range — where the old θ² form read γ ≲ θ³,
i.e. θ ≳ γ^{1/3}.
One polynomial power of 1/θ does remain inside D, through the moment
exponent's rate branch 64r(log 3r + c₁r)/(sθ); it is exactly the power the
consumer's ε² = s²θ pays for, which is why γ^{1/2} and not γ^{1/3} is the
reachable exponent. No third source of 1/θ exists in the chain.
Scope #
Provider material: proved local helpers. Every transcendental step is an abstract-real private helper.
References #
- ABK26,
l.ratio.of.good.scales.for.mathcal.E, in particular the constant-selection sentence;p.concentration.for.scales, (the threshold9 s⁻¹C^{1/p}θ^{-1/p}).
1. The log-quantile step #
The log-quantile bound. θ^{-1/p} ≤ 3 as soon as the moment exponent
clears 1/θ.
This is the step the proved RatioTailArith.threshold_le_inv pays crudely as
θ^{-1/p} ≤ θ⁻¹. The honest requirement is only log(1/θ) ≤ p log 3, and
log(1/θ) ≤ 1/θ − 1 ≤ p − 1 ≤ p log 3. It is the only place the quantile
rpow is opened.
The Appendix-D threshold below the row normalizer's reciprocal, at the log-quantile reading.
The sharp twin of RatioTailArith.threshold_le_inv: the key condition is
27 D (1+C⋆) ≤ s', with no θ on the right, at the cost of the extra
requirement θ⁻¹ ≤ p on the moment exponent — which the lane's own p already
satisfies (inv_theta_le_g2MomentExponent).
2. The proved moment exponent already clears 1/θ #
The lane's own moment exponent exceeds θ⁻¹.
g2MomentExponent's rate branch is 64r(log 3r + c₁r)/(sθ), and log 3r ≥ 1,
r ≥ 1, s ≤ 1, so it is at least 64/θ. Hence the log-quantile step
rpow_neg_inv_le_three is available at the unchanged moment exponent: the
sharp threshold costs no new branch and no new hypothesis.
3. The sharp threshold and its two constants #
The θ-free ε²-threshold of the 𝒢₂ proportion lane.
g2ThresholdSharp d r s θ c₁ = 108(1+C⋆)·D, with D = g2Normalizer … the
lane's own Appendix-D normalizer, unchanged. Compare the proved
G2ThresholdArith.g2Threshold … = 36(1+C⋆)·D/θ: the constant is tripled and
the divisor θ is gone. The two are therefore related by g2ThresholdSharp = 3θ · g2Threshold, so the sharp threshold is the smaller one exactly when θ < 1/3 — the small-level regime the printed Theorem-C range lives in.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The d-only constant of the binding clause of the sharp threshold
condition: three times the proved g2ThresholdConstOne.
Equations
Instances For
The d-only constant of the exponentially small clause of the sharp
threshold condition: three times the proved g2ThresholdConstTwo.
Equations
Instances For
4. The sufficient parameter condition #
The sharp ε-threshold is met under two closed parameter conditions.
(1) 3κ₁(d) r² (1+c₁) C² γ ≤ θ c⋆² s⁵ ε²
(2) 3κ₂(d) r⁸ (1+c₁)⁴ exp(−2c⋆³/(Cγ)) ≤ θ⁴ s⁹ ε²
Each clause is the corresponding clause of the crude reading with one power
of θ removed from the right-hand side and the constant tripled. Clause (1) is the binding one;
at the consumer's coupling ε² = s²θ
it reads γ ≲ θ², i.e. θ ≳ γ^{1/2} — the printed Theorem-C range — where the
proved θ² form read γ ≲ θ³.
The second sharp clause in γ-power form. exp(−w) ≤ 5040/w⁷ at
w = 2c⋆³/(Cγ) turns the exponentially small clause into
(2') (945/8) κ₂(d) r⁸ (1+c₁)⁴ C⁷ γ⁷ ≤ θ⁴ c⋆²¹ s⁹ ε² ,
six powers of γ weaker than the binding clause (1), which is linear in γ.