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

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

Prefactor absorption for stretched-exponential bad-scale tails

The selected bad-scale tail still has a deterministic prefactor-gap condition. This file proves the real-variable fact behind its eventual discharge: linear/exponential-in-q prefactors are absorbed by a geometric stretched-exponential gap.

theorem HCPolySupport.Book.Ch05.Section57.tendsto_exp_neg_const_mul_pow {c ρ : ℝ} (hc : 0 < c) (hρ : 1 < ρ) : Filter.Tendsto (fun (n : ℕ) => Real.exp (-(c * ρ ^ n))) Filter.atTop (nhds 0)

theorem HCPolySupport.Book.Ch05.Section57.summable_linear_pow_mul_exp_neg_const_mul_pow {M W c ρ : ℝ} (hM : 0 < M) (hW : 0 < W) (hc : 0 < c) (hρ : 1 < ρ) : Summable fun (n : ℕ) => M * ((↑n + 1) * W ^ n) * Real.exp (-(c * ρ ^ n))

theorem HCPolySupport.Book.Ch05.Section57.tendsto_linear_pow_mul_exp_neg_const_mul_pow {M W c ρ : ℝ} (hM : 0 ≤ M) (hW : 0 < W) (hc : 0 < c) (hρ : 1 < ρ) : Filter.Tendsto (fun (n : ℕ) => M * ((↑n + 1) * W ^ n) * Real.exp (-(c * ρ ^ n))) Filter.atTop (nhds 0)

theorem HCPolySupport.Book.Ch05.Section57.exists_forall_ge_linear_pow_le_exp_const_mul_pow {M W c ρ : ℝ} (hM : 0 ≤ M) (hW : 0 < W) (hc : 0 < c) (hρ : 1 < ρ) : ∃ (Q : ℕ), ∀ (q : ℕ), Q ≤ q → M * ((↑q + 1) * W ^ q) ≤ Real.exp (c * ρ ^ q)

A linear/exponential prefactor is eventually bounded by the exponential of a positive geometric gap.

theorem HCPolySupport.Book.Ch05.Section57.exists_forall_ge_prefactor_le_exp_gap_of_linear_pow_bound {pref gap : ℕ → ℝ} {M W c ρ : ℝ} (hM : 0 ≤ M) (hW : 0 < W) (hc : 0 < c) (hρ : 1 < ρ) (hpref : ∀ (q : ℕ), pref q ≤ M * ((↑q + 1) * W ^ q)) (hgap : ∀ (q : ℕ), c * ρ ^ q ≤ gap q) : ∃ (Q : ℕ), ∀ (q : ℕ), Q ≤ q → pref q ≤ Real.exp (gap q)

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_nat_div_eq_inv_rpow_mul {B η : ℝ} (q : ℕ) (hB : 0 < B) : (3 ^ ↑q / B) ^ η = B ^ (-η) * (3 ^ η) ^ q

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_nat_div_gap_eq {Btail Blead η : ℝ} (q : ℕ) (hBlead : 0 < Blead) (hBtail : 0 < Btail) : (3 ^ ↑q / Blead) ^ η - (3 ^ ↑q / Btail) ^ η = (Blead ^ (-η) - Btail ^ (-η)) * (3 ^ η) ^ q

theorem HCPolySupport.Book.Ch05.Section57.inv_rpow_sub_pos_of_lt {Btail Blead η : ℝ} (hBlead : 0 < Blead) (hBtail : 0 < Btail) (hη : 0 < η) (hlt : Blead < Btail) : 0 < Blead ^ (-η) - Btail ^ (-η)

theorem HCPolySupport.Book.Ch05.Section57.geometric_gap_le_rpow_three_nat_div_gap {Btail Blead η c ρ : ℝ} {q : ℕ} (hBlead : 0 < Blead) (hBtail : 0 < Btail) (hc : c ≤ Blead ^ (-η) - Btail ^ (-η)) (hρ : ρ ≤ 3 ^ η) (hc_nonneg : 0 ≤ c) (hρ_nonneg : 0 ≤ ρ) : c * ρ ^ q ≤ (3 ^ ↑q / Blead) ^ η - (3 ^ ↑q / Btail) ^ η

theorem HCPolySupport.Book.Ch05.Section57.max_zero_mul_le_mul_max_zero {a c : ℝ} (ha : 0 ≤ a) : max 0 (a * c) ≤ a * max 0 c

theorem HCPolySupport.Book.Ch05.Section57.selected_prefactor_le_linear_pow {Ctop Cbottom S Kbottom Kcrude w W M : ℝ} {q : ℕ} (hw_nonneg : 0 ≤ w) (hW_one : 1 ≤ W) (hwW : w ≤ W) (hM : max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (S * Kcrude) ≤ M) : max 0 Ctop + max 0 (↑(q + 1) * (Cbottom * w ^ q) * Kbottom) + max 0 (↑(q + 1) * (S * w ^ q) * Kcrude) ≤ M * ((↑q + 1) * W ^ q)

theorem HCPolySupport.Book.Ch05.Section57.exists_forall_ge_selected_prefactor_gap {Ctop Cbottom S Kbottom Kcrude w Blead Btail η : ℝ} (hBlead : 0 < Blead) (hBtail : 0 < Btail) (hη : 0 < η) (hlt : Blead < Btail) (hw_nonneg : 0 ≤ w) : ∃ (Q : ℕ), ∀ (q : ℕ), Q ≤ 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) ^ η)

Concrete eventual prefactor gap for the selected bad-scale component prefactors.