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

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

No-log fixed bad-pair probability bounds

This file restarts the bad-scale tail proof after removing the exponent-loss route. The estimates here keep finite maxima as probability prefactors instead of putting logarithmic factors into the stochastic scale.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHigh_badPairEvent_quenchedProbeEnvelope_le_card_mul_card_mul_exp_noLog {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 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 → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have x := αbad * ↑(m - q) - t * ↑(m - n); have ell := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have tau := min σ 2; have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * hΓ.thetaHat ^ 2; have T := Real.rpow 3 (-x); have lam := T / (2 * K * scale); ell < n → n < m → q ≤ m → 1 ≤ lam → MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau))

High-range fixed bad-pair estimate with explicit finite-union prefactors and no logarithmic scale inflation.

theorem HCPolySupport.Book.Ch05.Section57.shiftedHighBadPairProbability_le_cardSquaredExponential_annealedExponent {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have x := αbad * ↑(m - q) - t * ↑(m - n); have ell := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have tau := min σ 2; have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * hΓ.thetaHat ^ 2; have T := Real.rpow 3 (-x); have lam := T / (2 * K * scale); ell < n → n < m → q ≤ m → 1 ≤ lam → MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau))

Uniform-in-σ version of measureReal_shiftedHigh_badPairEvent_quenchedProbeEnvelope_le_card_mul_card_mul_exp_noLog.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrude_badPairEvent_quenchedProbeEnvelope_le_card_mul_card_mul_exp_noLog {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {N0 q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have x := αbad * ↑(m - q) - t * ↑(m - n); have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have scale := K * (C * hΓ.thetaHat ^ 2); have T := Real.rpow 3 (-x); have lam := T / scale; n < m → q ≤ m → 1 ≤ lam → MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ σ))

Crude fixed bad-pair estimate with explicit finite-union prefactors and no logarithmic scale inflation.