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

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

Minimal scale from the interpolated bad-scale tail

This file converts the eventual one-scale bad-scale estimate into the quantitative triadic minimal scale used in the quenched theorem. The only extra deterministic step is that the absolute tail at scale N dominates the shifted tail at N - Q, with the harmless replacement of the denominator by max 1 B.

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_sub_div_max_one_le_rpow_three_nat_div {Q N : ℕ} {B η : ℝ} (hB : 0 < B) (hη : 0 < η) : (Real.rpow 3 ↑(N - Q) / max 1 B) ^ η ≤ (3 ^ ↑N / B) ^ η

theorem HCPolySupport.Book.Ch05.Section57.exp_neg_rpow_three_nat_div_le_exp_neg_shifted_max_one {Q N : ℕ} {B η : ℝ} (hB : 0 < B) (hη : 0 < η) : Real.exp (-(3 ^ ↑N / B) ^ η) ≤ Real.exp (-(Real.rpow 3 ↑(N - Q) / max 1 B) ^ η)

theorem HCPolySupport.Book.Ch05.Section57.exists_shifted_quenchedLocalizedEstimate_interpolated {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; have B := max 1 Btail; 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → ∃ (Q : ℕ), have Bad := badScaleEvent Hshift t αbad; have X := quenchedMinimalScale Q Bad; IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (3 * 3 ^ Q * B) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (N0 + m) (N0 + n) e aω ≤ (3 ^ m / X aω) ^ (-αbad)

The finite-sigma interpolated bad-scale tail yields the shifted localized estimate above a quantitative minimal scale. The constants are chosen before the probability law; the terminal threshold Q and the normalizing denominator are allowed to depend on the law through the entry scale and thetaHat, as in the manuscript proof.