Elementary Gaussian bounds

A polynomial weight times a real Gaussian is bounded. This file records an explicit bound for (1 + r) ^ m * exp (-a r²) on r ≥ 0, the scalar estimate behind the decay of Gaussian Schwartz functions.

Main results

• TauCeti.one_add_pow_mul_exp_neg_mul_sq_le: an explicit bound for (1 + r) ^ m * exp (-a r²).

theorem TauCeti.one_add_pow_mul_exp_neg_mul_sq_le {a : ℝ} (ha : 0 < a) (m : ℕ) {r : ℝ} (hr : 0 ≤ r) : (1 + r) ^ m * Real.exp (-a * r ^ 2) ≤ ↑m.factorial / (a / 2) ^ m * Real.exp a

For 0 < a, the function r ↦ (1 + r) ^ m * exp (-a r²) is bounded on r ≥ 0 by the explicit constant m! / (a / 2) ^ m * exp a.