Abstract-real facts for the cutoff1 source contract

The exponential decay of the corrector after the support of ξ'_{m,k} beats every power of ε_m⁻¹. Pure real-variable lemmas: no objects appear here.

theorem AVenhance.Infra.Section5.Contracts.sb_pow_mul_exp_neg_le (n : ℕ) {c : ℝ} (hc : 0 < c) {y : ℝ} (hy : 0 ≤ y) : y ^ n * Real.exp (-(c * y)) ≤ ↑n.factorial / c ^ n

y^n e^{-cy} ≤ n!/c^n.

theorem AVenhance.Infra.Section5.Contracts.sb_rpow_mul_exp_neg_le {p c : ℝ} (hp : 0 ≤ p) (hc : 0 < c) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : ℝ), 0 ≤ y → y ^ p * Real.exp (-(c * y)) ≤ M

A real power times a decaying exponential is bounded.

theorem AVenhance.Infra.Section5.Contracts.sb_exp_decay_le {q δ c : ℝ} (hq : 0 ≤ q) (hδ : 0 < δ) (hc : 0 < c) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x Z : ℝ), 0 < x → c * x ^ (-(2 * δ)) ≤ Z → Real.exp (-Z) * (x ^ q)⁻¹ ≤ M * x ^ δ

Exponential decay at the scale x^{-2δ} beats x^{-q} up to x^δ.