exp_mul_le_cosh_add_mul_sinh — Mathlib

English

For any t with |t| ≤ 1 and any x, exp(t x) ≤ cosh x + t sinh x.

Русский

Для любого t с |t| ≤ 1 и любого x выполняется exp(t x) ≤ cosh x + t sinh x.

LaTeX

$$\forall t, x: |t| ≤ 1 \implies exp(t x) ≤ cosh x + t sinh x$$

Lean4

theorem exp_mul_le_cosh_add_mul_sinh {t : ℝ} (ht : |t| ≤ 1) (x : ℝ) : exp (t * x) ≤ cosh x + t * sinh x :=
  by
  rw [abs_le] at ht
  calc
    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
      (convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) <| by ring)
    _ = _ := by rw [cosh_eq, sinh_eq]; ring

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