abs_iteratedDeriv_cos_le_one — Mathlib

English

All derivatives of cos are uniformly bounded by 1 in absolute value.

Русский

Все производные от cos ограничены по модулю единицей.

LaTeX

$$$\\\\forall n \\in \\mathbb{N},\\forall x \\in \\\\mathbb{R}, \\\\left| \\\\frac{d^{n}}{dx^{n}} \\\\cos x \\right| \\le 1$$$

Lean4

theorem abs_iteratedDeriv_cos_le_one (n : ℕ) (x : ℝ) : |iteratedDeriv n cos x| ≤ 1 :=
  match n with
  | 0 => by simpa using Real.abs_cos_le_one x
  | 1 => by simpa using Real.abs_sin_le_one x
  | n + 2 => by simpa using abs_iteratedDeriv_cos_le_one n x

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