Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformBadScaleTailFinal #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Quantitative uniform-endpoint bad-scale tail #
This is the Γ∞ endpoint analogue of the finite-σ quantitative bad-scale
tail. The exponent is d; the crude-bottom deterministic cutoff contributes
an additional explicit threshold but no stochastic branch.
theorem
HCPolySupport.Book.Ch05.Section57.exists_quantitative_threshold_shiftedBadScaleEvent_quenchedProbeEnvelope_le_uniformEndpoint_tail
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ},
have K := quenchedProbeEnvelopeConst d;
have S := Finset.univ;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have ctop := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have η := ↑d;
have w := ↑(3 ^ d);
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ 2);
have Kbottom := weightedGeometricExpKernelConst w (ρbottom ^ η);
have W := max 1 w;
have M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom));
have ρgap := 3 ^ η;
have C₀ := 2 + Real.log W;
0 < t →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
t ≤ b →
∃ (R : ℕ),
(∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρgap / 2 * ↑q)) ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.params = params →
have N0 :=
annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) =>
quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2;
have Dcrude := K * Ccrude * hInf.thetaHat ^ 2;
have Den := uniformEndpointHighDenominator Dhigh Dcrude t η;
have Blead := Den * 3 ^ (L + 1);
have Btail := 2 * Blead;
have cgap := Blead ^ (-η) - Btail ^ (-η);
have Qpref :=
max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log cgap) / Real.log ρgap⌉₊);
have Qlead := ⌈Real.log Blead / Real.log 3⌉₊;
have Qcrude := ⌈⋯⌉₊;
have Qcut := ⌈(L + 1) / (1 - αbad / a) + 1⌉₊;
⋯