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

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

Selected-denominator bad-scale tail collapse

This file reattaches the deterministic collapse from BadScaleTailCollapse to the synchronized selected-denominator component theorem.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_interpolated_tail_of_prefactor_gap {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Btail : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q : ℕ}, 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 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 τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); 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 Alead := (3 ^ ↑q / Blead) ^ η; have Atail := (3 ^ ↑q / Btail) ^ η; have ρtop := 3 ^ ctop; have ρbottom := 3 ^ (τ * (t - αbad) / η); have ρcrude := 3 ^ (t - αbad); have Cbottom := Real.exp 1 * max 1 ↑S.card; have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ); have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η); have CcrudeBottom := ↑(q + 1) * (↑S.card * w ^ q) * weightedGeometricExpKernelConst w (ρcrude ^ σ); 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → 0 < Btail → 1 ≤ 3 ^ ↑q / Blead → ⋯ → ⋯

The selected-denominator bad-scale estimate collapsed to one finite-sigma tail, up to the deterministic large-scale and prefactor-gap inequalities.

theorem HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_interpolated_tail {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ) (Ccrude : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ ∀ {t αbad Btail : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q : ℕ}, 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 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 τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); 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 Alead := (3 ^ ↑q / Blead) ^ η; have Atail := (3 ^ ↑q / Btail) ^ η; have ρtop := 3 ^ ctop; have ρbottom := 3 ^ (τ * (t - αbad) / η); have ρcrude := 3 ^ (t - αbad); have Cbottom := Real.exp 1 * max 1 ↑S.card; have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ); have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η); have CcrudeBottom := ↑(q + 1) * (↑S.card * w ^ q) * weightedGeometricExpKernelConst w (ρcrude ^ σ); 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → 0 < Btail → ⋯

Uniform-in-σ version of measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_interpolated_tail_of_prefactor_gap.

theorem HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_interpolated_tail_of_thresholds {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Btail : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q : ℕ}, 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 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 τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); 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 Alead := (3 ^ ↑q / Blead) ^ η; have Atail := (3 ^ ↑q / Btail) ^ η; have ρtop := 3 ^ ctop; have ρbottom := 3 ^ (τ * (t - αbad) / η); have ρcrude := 3 ^ (t - αbad); have Cbottom := Real.exp 1 * max 1 ↑S.card; have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ); have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η); have CcrudeBottom := ↑(q + 1) * (↑S.card * w ^ q) * weightedGeometricExpKernelConst w (ρcrude ^ σ); 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → 0 < Btail → ⌈Real.log Blead / Real.log 3⌉₊ ≤ q → ⋯ → ⋯

The same tail collapse after discharging the deterministic lower bound on the lead tail parameter and the crude-top cutoff by explicit ceiling thresholds. The prefactor gap is the only remaining large-scale condition.

theorem HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_interpolatedTail_of_thresholds {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ) (Ccrude : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ ∀ {t αbad Btail : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q : ℕ}, 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 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 τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); 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 Alead := (3 ^ ↑q / Blead) ^ η; have Atail := (3 ^ ↑q / Btail) ^ η; have ρtop := 3 ^ ctop; have ρbottom := 3 ^ (τ * (t - αbad) / η); have ρcrude := 3 ^ (t - αbad); have Cbottom := Real.exp 1 * max 1 ↑S.card; have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ); have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η); have CcrudeBottom := ↑(q + 1) * (↑S.card * w ^ q) * weightedGeometricExpKernelConst w (ρcrude ^ σ); 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → 0 < Btail → ⋯

Uniform-in-σ version of shiftedBadScaleProbability_le_interpolated_tail_of_thresholds.