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

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

The localized high-top branch at the uniform endpoint

The high-top branch uses the finite Γ_2 consequence of the uniform endpoint. Since the localized top exponent is 2 * d / 2, this branch already has the endpoint Γ_d exponent after a deterministic denominator rewrite.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighTopBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∀ {q : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; 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 Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2; have A := 3 ^ (↑q - (L + 1)) / Den; have ρtop := 3 ^ ctop; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 0 < Den → Dhigh ^ 2 ≤ Den ^ η → 1 ≤ A → MeasureTheory.Measure.real P (highTopBadScaleEvent Hshift K a t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ 2))

Endpoint high-top component estimate after rewriting the localized Γ_2 branch with the endpoint exponent d.