Coarse-graining support: Support.Book.Ch05.Theorems.Section57.AbsoluteScaleCompressionFinal #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Final absolute-scale compression #
This file contains the last deterministic compression steps for the absolute minimal scale in the quenched homogenization theorem.
theorem
HCPolySupport.Book.Ch05.Section57.explicit_union_prefactor_le_exp_logSq
{d : ℕ}
[NeZero d]
{σ Cfluct CcrudeShift Csmall a t : ℝ}
{Runion : ℕ}
(hσ : 0 < σ)
(ha : 0 < a)
(ht : 0 < t)
:
have K := quenchedProbeEnvelopeConst d;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have ρgap := 3 ^ η;
∃ (Cscale : ℝ),
0 < Cscale ∧ ∀ (θ : ℝ),
0 < θ →
have Dhigh := 2 * K * Cfluct * θ ^ 2;
have Dcrude := K * CcrudeShift * θ ^ 2;
have DenShift := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have Ohigh := τ * b * (L + 1) / η;
have Ocrude := σ * t * (L + 1) / η;
have BleadShift := max (DenShift * 3 ^ Ohigh) (DenShift * 3 ^ Ocrude);
have BtailShift := 2 * BleadShift;
have scaleSmall := K * (Csmall * θ ^ 2);
have BleadSmall := smallBottomTailDenominator scaleSmall η σ;
have BtailSmall := 2 * BleadSmall;
have BleadUnion := max BtailShift BtailSmall;
have BtailUnion := 2 * BleadUnion;
have cgapUnion := BleadUnion ^ (-η) - BtailUnion ^ (-η);
have Qunion := max ⌈max 0 (Real.log 2)⌉₊ (max Runion ⌈2 * max 0 (-Real.log cgapUnion) / Real.log ρgap⌉₊);
3 * 3 ^ Qunion * max 1 BtailUnion ≤ Real.exp (Cscale * Real.log (2 + θ) ^ 2)
The union cutoff in the absolute bad-scale estimate is still polynomial in
theta, hence is also compressed by the manuscript exp(C log^2) envelope.
theorem
HCPolySupport.Book.Ch05.Section57.absolute_prefactor_le_branch_product
{N0 Qshift Qsmall Qunion : ℕ}
{Bshift Bsmall Bunion : ℝ}
(hBshift : 1 ≤ Bshift)
(hBsmall : 1 ≤ Bsmall)
(hBunion : 1 ≤ Bunion)
:
The absolute prefactor is dominated by the product of the shifted, small-bottom, and union prefactors.
theorem
HCPolySupport.Book.Ch05.Section57.explicit_absoluteMinimalScale_prefactor_le_exp_logSq
{d : ℕ}
[NeZero d]
{σ Cfluct CcrudeShift Csmall a t α CentryScale : ℝ}
{Rshift Rsmall Runion : ℕ}
(hσ : 0 < σ)
(hCfluct : 0 < Cfluct)
(hCcrudeShift : 0 < CcrudeShift)
(hCsmall : 0 < Csmall)
(ha : 0 < a)
(ht : 0 < t)
(hαt : α < t)
(hCentryScale : 0 < CentryScale)
:
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 - α) (min (↑d / 2 - α) (min ((t - α) * (1 + ↑d / 2 / a)) (↑d / 2 - α * (1 + ↑d / 2 / a))));
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - α) / η);
have ρcrude := 3 ^ (t - α);
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 Mshift := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (↑S.card * Kcrude));
have ρgap := 3 ^ η;
∃ (Cscale : ℝ),
0 < Cscale ∧ ∀ {θ : ℝ} {N0 : ℕ},
0 < θ →
3 ^ N0 ≤ Real.exp (CentryScale * Real.log (2 + θ) ^ 2) →
have Dhigh := 2 * K * Cfluct * θ ^ 2;
have Dcrude := K * CcrudeShift * θ ^ 2;
have DenShift := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have Ohigh := τ * b * (L + 1) / η;
have Ocrude := σ * t * (L + 1) / η;
have BleadShift := max (DenShift * 3 ^ Ohigh) (DenShift * 3 ^ Ocrude);
have BtailShift := 2 * BleadShift;
have cgapShift := BleadShift ^ (-η) - BtailShift ^ (-η);
have QprefShift :=
max ⌈max 0 (Real.log Mshift)⌉₊ (max Rshift ⌈2 * max 0 (-Real.log cgapShift) / Real.log ρgap⌉₊);
have QleadShift := ⌈Real.log BleadShift / Real.log 3⌉₊;
have QcutShift := ⌈(L + 1) / (1 - α / a) + 1⌉₊;
have Qshift := max QprefShift (max QleadShift QcutShift);
have scaleSmall := K * (Csmall * θ ^ 2);
have ρsmall := 3 ^ (t - α);
have Ksmall := weightedGeometricExpKernelConst w (ρsmall ^ σ);
have prefSmall := ↑N0 * ↑S.card * w ^ N0;
have Msmall := max 1 (max 0 (prefSmall * Ksmall));
have BleadSmall := smallBottomTailDenominator scaleSmall η σ;
have BtailSmall := 2 * BleadSmall;
have cgapSmall := BleadSmall ^ (-η) - BtailSmall ^ (-η);
have QprefSmall :=
max ⌈max 0 (Real.log Msmall)⌉₊ (max Rsmall ⌈2 * max 0 (-Real.log cgapSmall) / Real.log ρgap⌉₊);
have QleadSmall := ⌈Real.log BleadSmall / Real.log 3⌉₊;
have Qsmall := max QprefSmall QleadSmall;
have BleadUnion := max BtailShift BtailSmall;
have BtailUnion := 2 * BleadUnion;
have cgapUnion := BleadUnion ^ (-η) - BtailUnion ^ (-η);
have Qunion := max ⌈max 0 (Real.log 2)⌉₊ ⋯;
have Q := max Qshift (max Qsmall Qunion);
⋯
Final deterministic compression of the explicit absolute minimal-scale normalization.