Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformScaleCompressionFinal #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scale compression at the uniform endpoint #
This file compresses the explicit Γ∞ endpoint minimal-scale normalization to
the manuscript exp(C log^2(2 + thetaHat)) envelope.
theorem
HCPolySupport.Book.Ch05.Section57.explicit_uniformEndpoint_minimalScale_prefactor_le_exp_logSq
{d : ℕ}
[NeZero d]
{Cfluct Ccrude a t αbad : ℝ}
{R : ℕ}
(hCfluct : 0 < Cfluct)
(hCcrude : 0 < Ccrude)
(ha : 0 < a)
(ht : 0 < t)
(htb : t ≤ ↑d / 2)
:
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 η := ↑d;
have w := ↑(3 ^ d);
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ 2);
have Kbottom := weightedGeometricExpKernelConst w (ρbottom ^ η);
have M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom));
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 := uniformEndpointHighDenominator Dhigh Dcrude t η;
have Blead := Den * 3 ^ (L + 1);
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 Qcrude := ⌈(Real.log Dcrude + t * (L + 1) * Real.log 3) / (t * Real.log 3)⌉₊;
have Q := max Qpref (max Qlead (max Qcrude Qcut));
3 * 3 ^ Q * B ≤ Real.exp (Cscale * Real.log (2 + θ) ^ 2)