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

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

Selecting the intermediate scale in high bad-pair estimates

This file combines the deterministic ceiling choice for ℓ with the fixed-pair high-scale probability estimate.

theorem HCPolySupport.Book.Ch05.Section57.three_mul_log_descendantsAtScale_originCube_nat_card_pos {d : ℕ} [NeZero d] {m n : ℕ} (hnm : n < m) : 0 < 3 * Real.log ↑(descendantsAtScale (originCube d ↑m) ↑n).card

theorem HCPolySupport.Book.Ch05.Section57.shiftedHighBadPairFluctuationScale_pos {d : ℕ} [NeZero d] {σ Cfluct : ℝ} (hσ_pos : 0 < σ) (hCfluct : 0 < Cfluct) {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {N0 m n ℓ : ℕ} (hnm : n < m) : 0 < quenchedProbeEnvelopeConst d * ((3 * Real.log ↑Finset.univ.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑(descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n)).card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2)))

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

High-scale fixed-pair estimate with the deterministic intermediate scale chosen by a logarithmic ceiling. The remaining hypothesis is the genuinely stochastic threshold-size condition for the fluctuation scale.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHigh_badPairEvent_quenchedProbeEnvelope_le_exp_of_natCeil_ratio {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 ℓ := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have A := K * ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2))); have T := Real.rpow 3 (-x); ℓ < n → n < m → q ≤ m → 1 ≤ T / (2 * A) → MeasureTheory.Measure.real P (badPairEvent (fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω) t αbad q m n) ≤ Real.exp (-(T / (2 * A)) ^ min σ 2)

High-scale fixed-pair estimate after choosing the tail parameter s = T / (2A), where A is the fluctuation scale and T is the post-discount threshold.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHigh_badPairEvent_quenchedProbeEnvelope_le_exp_of_natCeil_ratio_natScale {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 ℓ := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have A := K * ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(n - ℓ)) * hΓ.thetaHat ^ 2))); have T := Real.rpow 3 (-x); ℓ < n → n < m → q ≤ m → 1 ≤ T / (2 * A) → MeasureTheory.Measure.real P (badPairEvent (fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω) t αbad q m n) ≤ Real.exp (-(T / (2 * A)) ^ min σ 2)

The selected-ratio high-pair estimate with the shifted scale difference simplified to the manuscript form n - ℓ.

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

High-pair estimate fed by any deterministic lower bound on the selected tail parameter.