Coarse-graining support: Support.Book.Ch05.Theorems.Section51.ExponentAbsorption

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

Exponent absorption for the main annealed convergence theorem

This file contains the pure real-arithmetic step which turns a bound with a fixed prefactor into the note-facing bound with unit prefactor, after shrinking the algebraic exponent.

theorem HCPolySupport.Book.Ch05.Section51.quarter_le_rpow_three_neg_mul_of_mul_nat_le_one {α : ℝ} {n : ℕ} (hαn : α * ↑n ≤ 1) : 1 / 4 ≤ Real.rpow 3 (-α * ↑n)

theorem HCPolySupport.Book.Ch05.Section51.prefactor_decay_le_half_exponent_decay_of_large {α₀ K : ℝ} {n : ℕ} (hα₀ : 0 < α₀) (hlarge : Real.log (max (4 * K) 1) / (α₀ / 2 * Real.log 3) ≤ ↑n) : 4 * K * Real.rpow 3 (-α₀ * ↑n) ≤ Real.rpow 3 (-(α₀ / 2) * ↑n)

theorem HCPolySupport.Book.Ch05.Section51.mul_nat_le_one_of_le_inverse_succ {α : ℝ} {R n : ℕ} (hα : α ≤ (↑(R + 1))⁻¹) (hn : n ≤ R) : α * ↑n ≤ 1