Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleTailFinal

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Eventual shifted bad-scale tail

This file combines the selected bad-scale tail, deterministic threshold selection, and prefactor absorption. The output is still shifted by the annealed entry scale; the next layer converts this eventual bad-scale bound into a tail bound for the random minimal scale.

theorem HCPolySupport.Book.Ch05.Section57.exists_threshold_shiftedBadScaleEvent_quenchedProbeEnvelope_le_interpolated_tail {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2; have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2; have Den := mixedBottomTailDenominator Dhigh Dcrude η τ σ; have Ohigh := τ * b * (L + 1) / η; have Ocrude := σ * t * (L + 1) / η; have Blead := max (Den * 3 ^ Ohigh) (Den * 3 ^ Ocrude); have Btail := 2 * Blead; 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → ∃ (Q : ℕ), ∀ (q : ℕ), Q ≤ q → MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ Real.exp (-(3 ^ ↑q / Btail) ^ η)