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

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

Quantitative prefactor absorption

The earlier prefactor absorption lemma used a Tendsto argument and returned only an eventual threshold. This file keeps the same deterministic absorption, but makes the law-dependent part of the threshold explicit through max 0 (-log c), where c is the geometric gap coefficient. Constants coming from the finite probe family remain in one law-independent natural threshold.

theorem HCPolySupport.Book.Ch05.Section57.linear_le_exp_linear_eventually {C γ : ℝ} (hC : 0 ≤ C) (hγ : 0 < γ) : ∃ (R : ℕ), ∀ (q : ℕ), R ≤ q → C * ↑q ≤ Real.exp (γ * ↑q)

theorem HCPolySupport.Book.Ch05.Section57.linear_prefactor_le_exp_linear {M W C₀ : ℝ} {q : ℕ} (hM : 1 ≤ M) (hW : 1 ≤ W) (hlogM : Real.log M ≤ ↑q) (hC₀ : 2 + Real.log W ≤ C₀) : M * ((↑q + 1) * W ^ q) ≤ Real.exp (C₀ * ↑q)

theorem HCPolySupport.Book.Ch05.Section57.exp_half_log_mul_le_const_mul_pow_of_log_gap {c ρ : ℝ} {q : ℕ} (hc : 0 < c) (hρ : 1 < ρ) (hq : 2 * max 0 (-Real.log c) / Real.log ρ ≤ ↑q) : Real.exp (Real.log ρ / 2 * ↑q) ≤ c * ρ ^ q

theorem HCPolySupport.Book.Ch05.Section57.linear_prefactor_le_exp_const_mul_pow_of_large {M W C₀ c ρ : ℝ} {R q : ℕ} (hM : 1 ≤ M) (hW : 1 ≤ W) (hc : 0 < c) (hρ : 1 < ρ) (hC₀ : 2 + Real.log W ≤ C₀) (hRlin : ∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρ / 2 * ↑q)) (hqM : ⌈max 0 (Real.log M)⌉₊ ≤ q) (hqR : R ≤ q) (hqc : ⌈2 * max 0 (-Real.log c) / Real.log ρ⌉₊ ≤ q) : M * ((↑q + 1) * W ^ q) ≤ Real.exp (c * ρ ^ q)

theorem HCPolySupport.Book.Ch05.Section57.exists_forall_ge_selected_prefactor_gap_quantitative {Ctop Cbottom S Kbottom Kcrude w Blead Btail η : ℝ} (hBlead : 0 < Blead) (hBtail : 0 < Btail) (hη : 0 < η) (hlt : Blead < Btail) (hw_nonneg : 0 ≤ w) : have W := max 1 w; have M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (S * Kcrude)); have c := Blead ^ (-η) - Btail ^ (-η); have ρ := 3 ^ η; have C₀ := 2 + Real.log W; ∃ (R : ℕ), (∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρ / 2 * ↑q)) ∧ ∀ (q : ℕ), max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log c) / Real.log ρ⌉₊) ≤ q → max 0 Ctop + max 0 (↑(q + 1) * (Cbottom * w ^ q) * Kbottom) + max 0 (↑(q + 1) * (S * w ^ q) * Kcrude) ≤ Real.exp ((3 ^ ↑q / Blead) ^ η - (3 ^ ↑q / Btail) ^ η)

Quantitative version of exists_forall_ge_selected_prefactor_gap. The integer R is law-independent; all law dependence in the threshold is carried by the explicit term involving -log c.

theorem HCPolySupport.Book.Ch05.Section57.exists_forall_ge_selected_prefactor_gap_quantitative_uniform {Ctop Cbottom S Kbottom Kcrude w η : ℝ} (hη : 0 < η) (hw_nonneg : 0 ≤ w) : have W := max 1 w; have M := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (S * Kcrude)); have ρ := 3 ^ η; have C₀ := 2 + Real.log W; ∃ (R : ℕ), (∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρ / 2 * ↑q)) ∧ ∀ {Blead Btail : ℝ}, 0 < Blead → 0 < Btail → Blead < Btail → have c := Blead ^ (-η) - Btail ^ (-η); ∀ (q : ℕ), max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log c) / Real.log ρ⌉₊) ≤ q → max 0 Ctop + max 0 (↑(q + 1) * (Cbottom * w ^ q) * Kbottom) + max 0 (↑(q + 1) * (S * w ^ q) * Kcrude) ≤ Real.exp ((3 ^ ↑q / Blead) ^ η - (3 ^ ↑q / Btail) ^ η)

Uniform-in-denominator version of the quantitative prefactor gap. The integer R is selected before the geometric gap coefficient, hence before any probability law in downstream applications.