one_add_mul_le_cos — Mathlib

English

For -(π/2) ≤ x ≤ 0, 1 + (2/π) x ≤ cos x.

Русский

Пусть -(π/2) ≤ x ≤ 0. Тогда 1 + 2x/π ≤ cos x.

LaTeX

$$$\forall x \in \mathbb{R}, -(\pi/2) \le x \le 0 \Rightarrow 1 + \dfrac{2}{\pi} x \le \cos x$$$

Lean4

/-- Half of **Jordan's inequality** for `cos` and negative values. -/
theorem one_add_mul_le_cos (hx₀ : -(π / 2) ≤ x) (hx : x ≤ 0) : 1 + 2 / π * x ≤ cos x := by
  simpa using one_sub_mul_le_cos (x := -x) (by linarith) (by linarith)

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