cosh_le_exp_half_sq — Mathlib

English

For every real x, one has cosh x ≤ exp(x^2/2).

Русский

Для каждого действительного x выполняется неравенство cosh x ≤ exp(x^2/2).

LaTeX

$$$\\cosh x \leq e^{x^{2}/2}$$$

Lean4

theorem cosh_le_exp_half_sq (x : ℝ) : cosh x ≤ exp (x ^ 2 / 2) :=
  by
  rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum]
  refine x.hasSum_cosh.summable.tsum_le_tsum (fun i ↦ ?_) <| expSeries_summable' (x ^ 2 / 2)
  simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]
  gcongr
  norm_cast
  exact Nat.two_pow_mul_factorial_le_factorial_two_mul _

Похожие утверждения