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

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

Deterministic compression for the absolute quenched scale

This file contains the deterministic estimates used to compress the explicit absolute minimal-scale normalization to the manuscript envelope exp(C log^2(2 + thetaHat)).

theorem HCPolySupport.Book.Ch05.Section57.const_mul_entry_rpow_mul_rpow_max_one_le_exp_logSq {A G θ Centry r p : ℝ} (hA : 0 < A) (hG : 1 ≤ G) (hθ : 0 ≤ θ) (hCentry : 0 < Centry) (hr : 0 ≤ r) (hp : 0 ≤ p) (hentry : G ≤ Real.exp (Centry * Real.log (2 + θ) ^ 2)) : ∃ (C : ℝ), 0 < C ∧ A * G ^ r * max 1 θ ^ p ≤ Real.exp (C * Real.log (2 + θ) ^ 2)

An entry-scale factor times a fixed polynomial in theta is absorbed by the manuscript exp(C log^2(2 + theta)) envelope.

theorem HCPolySupport.Book.Ch05.Section57.nat_cast_le_pow_three_nat (N : ℕ) : ↑N ≤ 3 ^ N

Natural entry scales are dominated by their base-three exponential.

theorem HCPolySupport.Book.Ch05.Section57.pow_three_natCeil_max_zero_log_le_const_mul_rpow_of_le {M A G p : ℝ} (hM_one : 1 ≤ M) (hA_pos : 0 < A) (hG_one : 1 ≤ G) (hM_le : M ≤ A * G ^ p) : 3 ^ ⌈max 0 (Real.log M)⌉₊ ≤ 3 * A ^ Real.log 3 * G ^ (p * Real.log 3)

A logarithmic ceiling cutoff is polynomial in any positive upper bound for the underlying quantity.

theorem HCPolySupport.Book.Ch05.Section57.smallBottom_M_le_const_mul_entry_power {d N0 : ℕ} {Ksmall : ℝ} (hKsmall : 0 ≤ Ksmall) : have S := Finset.univ; have w := ↑(3 ^ d); have G := 3 ^ N0; have pref := ↑N0 * ↑S.card * w ^ N0; have M := max 1 (max 0 (pref * Ksmall)); have A := max 1 (↑S.card * Ksmall); M ≤ A * G ^ (↑d + 1)

The small-bottom prefactor Msmall is polynomial in the entry-scale factor 3 ^ N0.

theorem HCPolySupport.Book.Ch05.Section57.explicit_threshold_prefactor_le_exp_logSq_of_Blead_le_poly {η A p M : ℝ} {R Qcut : ℕ} (hη : 0 < η) (hA : 0 < A) (hp : 0 ≤ p) : ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ (θ : ℝ), 0 ≤ θ → ∀ (Blead : ℝ), 1 ≤ Blead → Blead ≤ A * max 1 θ ^ p → have Btail := 2 * Blead; 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 * max 1 Btail ≤ Real.exp (Cscale * Real.log (2 + θ) ^ 2)

If the selected leading denominator is polynomial in theta, then the explicit prefactor-gap threshold attached to it is compressed by the manuscript exp(C log^2(2 + theta)) envelope.

theorem HCPolySupport.Book.Ch05.Section57.explicit_smallBottom_prefactor_le_exp_logSq {d : ℕ} [NeZero d] {σ Csmall t α CentryScale : ℝ} {Rsmall : ℕ} (hσ : 0 < σ) (hCsmall : 0 < Csmall) (ht : 0 < t) (hαt : α < t) (hCentryScale : 0 < CentryScale) : have K := quenchedProbeEnvelopeConst d; have S := Finset.univ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); have ρsmall := 3 ^ (t - α); have Ksmall := weightedGeometricExpKernelConst w (ρsmall ^ σ); have ρgap := 3 ^ η; ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {θ : ℝ} {N0 : ℕ}, 0 < θ → 3 ^ N0 ≤ Real.exp (CentryScale * Real.log (2 + θ) ^ 2) → have scaleSmall := K * (Csmall * θ ^ 2); 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; 3 * 3 ^ (N0 + Qsmall) * max 1 BtailSmall ≤ Real.exp (Cscale * Real.log (2 + θ) ^ 2)

Compress the explicit small-bottom threshold once the annealed entry factor has already been compressed.