Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ScaleCompressionFinal #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Final deterministic scale compression #
This file compresses the explicit quantitative minimal-scale normalization
3 * 3^Q * B to the manuscript envelope exp(C log^2(2 + thetaHat)).
theorem
HCPolySupport.Book.Ch05.Section57.one_le_mixedBottomTailDenominator
{Dhigh Dcrude η τ σ : ℝ}
(hη : 0 < η)
(hτ : 0 ≤ τ)
:
theorem
HCPolySupport.Book.Ch05.Section57.explicit_minimalScale_prefactor_le_exp_logSq
{d : ℕ}
[NeZero d]
{σ Cfluct Ccrude a t αbad : ℝ}
{R : ℕ}
(hσ : 0 < σ)
(hCfluct : 0 < Cfluct)
(hCcrude : 0 < Ccrude)
(ha : 0 < a)
(ht : 0 < t)
:
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 M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (↑S.card * Kcrude));
have Qcut := ⌈(L + 1) / (1 - αbad / a) + 1⌉₊;
∃ (Cscale : ℝ),
0 < Cscale ∧ ∀ (θ : ℝ),
0 < θ →
have Dhigh := 2 * K * Cfluct * θ ^ 2;
have Dcrude := K * Ccrude * θ ^ 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;
have cgap := Blead ^ (-η) - Btail ^ (-η);
have ρgap := 3 ^ η;
have Qpref := max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log cgap) / Real.log ρgap⌉₊);
have Qlead := ⌈Real.log Blead / Real.log 3⌉₊;
have Q := max Qpref (max Qlead Qcut);
3 * 3 ^ Q * B ≤ Real.exp (Cscale * Real.log (2 + θ) ^ 2)