Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleMinimalQuantitative #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Quantitative minimal scale from the interpolated bad-scale tail #
This file keeps the deterministic prefactor threshold selected before the probability law. It is the quantitative replacement for the eventual minimal-scale theorem, and is the layer used in the final compression to the manuscript stochastic-integrability statement.
theorem
HCPolySupport.Book.Ch05.Section57.exists_quantitative_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 : ℝ},
have K := quenchedProbeEnvelopeConst d;
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 ρ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 Kbottom := weightedGeometricExpKernelConst w (ρbottom ^ η);
have Kcrude := weightedGeometricExpKernelConst w (ρcrude ^ σ);
have W := max 1 w;
have M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (↑S.card * Kcrude));
have ρgap := 3 ^ η;
have C₀ := 2 + Real.log W;
0 < t →
t ≤ b →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
∃ (R : ℕ),
(∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρgap / 2 * ↑q)) ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
have N0 :=
annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) =>
quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
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 := ⋯;
⋯
The finite-sigma interpolated bad-scale tail yields the shifted
localized estimate above an explicit quantitative minimal scale. The
constant R controlling the deterministic prefactor is selected before the
probability law.