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

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

Compression of the explicit bad-scale threshold

The quantitative tail theorem exposes three deterministic cutoffs. This file collapses them to a fixed polynomial in the selected denominator Blead, after the final tail denominator is chosen as 2 * Blead.

theorem HCPolySupport.Book.Ch05.Section57.pow_three_nat_mono {m n : ℕ} (hmn : m ≤ n) : 3 ^ m ≤ 3 ^ n

theorem HCPolySupport.Book.Ch05.Section57.pow_three_natCeil_log_div_log_le_three_mul_self {x : ℝ} (hx : 1 ≤ x) : 3 ^ ⌈Real.log x / Real.log 3⌉₊ ≤ 3 * x

theorem HCPolySupport.Book.Ch05.Section57.pow_three_nat_add (a b : ℕ) : 3 ^ (a + b) = 3 ^ a * 3 ^ b

theorem HCPolySupport.Book.Ch05.Section57.pow_three_nat_add_five (a b c d e : ℕ) : 3 ^ (a + b + c + d + e) = 3 ^ a * 3 ^ b * 3 ^ c * 3 ^ d * 3 ^ e

theorem HCPolySupport.Book.Ch05.Section57.pow_three_explicit_threshold_le_const_mul_Blead_four {M η Blead : ℝ} {R Qcut : ℕ} (hη : 0 < η) (hBlead : 1 ≤ Blead) : 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); have Cgap := 2 * max 0 (-Real.log (1 - 2 ^ (-η))) / (η * Real.log 3); have C := 18 * 3 ^ (⌈max 0 (Real.log M)⌉₊ + R + Qcut) * Real.exp (Real.log 3 * Cgap); 3 ^ Q * max 1 Btail ≤ C * Blead ^ 4