Real exponential and logarithmic estimates used in the analytic KAM bounds.

theorem KamProject.Arnold1963.rpow_mul_exp_neg_le {x v : ℝ} (hx : 0 < x) (hv : 0 < v) : x ^ v * Real.exp (-x) ≤ (v / Real.exp 1) ^ v

theorem KamProject.Arnold1963.rpow_le_scaled_exp {m v δ : ℝ} (hm : 0 < m) (hv : 0 < v) (hδ : 0 < δ) : m ^ v ≤ (v / Real.exp 1) ^ v * δ ^ (-v) * Real.exp (m * δ)

theorem KamProject.Arnold1963.log_le_rpow {x v : ℝ} (hx : 0 < x) (hv : 0 < v) : Real.log x ≤ v / Real.exp 1 * x ^ (1 / v)

theorem KamProject.Arnold1963.rpow_mul_exp_neg_mul_le {m v δ : ℝ} (hm : 0 < m) (hv : 0 < v) (hδ : 0 < δ) : m ^ v * Real.exp (-(m * δ)) ≤ (v / Real.exp 1) ^ v * δ ^ (-v)

theorem KamProject.Arnold1963.log_inv_le_rpow {δ v : ℝ} (hδ : 0 < δ) (hv : 0 < v) : Real.log (1 / δ) ≤ v / Real.exp 1 * δ ^ (-(1 / v))

theorem KamProject.Arnold1963.half_le_one_sub_exp_neg {δ : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) : δ / 2 ≤ 1 - Real.exp (-δ)