Poly Exp Bounds

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Heat.exp_poly_bound {k : ℕ} {a : ℝ} (ha : 0 ≤ a) : a ^ k * Real.exp (-a) ≤ ↑k.factorial

For nonnegative a and k : ℕ, a ^ k * exp(-a) ≤ k!.

theorem CKN.Foundation.Heat.one_add_pow_exp_neg_le {n : ℕ} {a : ℝ} (ha : 0 ≤ a) : (1 + a) ^ n * Real.exp (-a) ≤ 2 ^ (n - 1) * (1 + ↑n.factorial)

For nonnegative a and n : ℕ, (1 + a)^n * exp(-a) ≤ 2^(n-1) * (1 + n!).

theorem CKN.Foundation.Heat.heat_prefactor_le {t : ℝ} (ht : 0 < t) : (4 * Real.pi * t) ^ (-3 / 2) ≤ √t ^ (-3)

For positive time t, the heat prefactor (4πt)^(-3/2) is bounded by (√t)^(-3).

theorem CKN.Foundation.Heat.heat_rpow_neg_three (z : ℝ) (hz : 0 < z) : z ^ (-3) = (z ^ 3)⁻¹

For positive z, z^(-3) equals (z^3)⁻¹.