cos_le_one_sub_mul_cos_sq — Mathlib

English

If |x| ≤ π, then cos x ≤ 1 − (2/π^2) x^2.

Русский

Если |x| ≤ π, то cos x ≤ 1 − (2/π^2) x^2.

LaTeX

$$$|x| \le \pi \Rightarrow \cos x \le 1 - \dfrac{2}{\pi^2} x^2$$$

Lean4

theorem cos_le_one_sub_mul_cos_sq (hx : |x| ≤ π) : cos x ≤ 1 - 2 / π ^ 2 * x ^ 2 :=
  by
  wlog hx₀ : 0 ≤ x
  case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀
  rw [abs_of_nonneg hx₀] at hx
  have : x / π ≤ sin (x / 2) := by simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)
  have := (pow_le_pow_left₀ (by positivity) this 2).trans_eq (sin_sq_eq_half_sub _)
  ring_nf at this ⊢
  linarith

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