hasStrictDerivAt_sin — Mathlib

English

The complex sine function is everywhere strictly differentiable with derivative cos x.

Русский

Комплексная функция синуса во всех точках строго дифференцируема, производная равна cos x.

LaTeX

$$$$\forall x \in \mathbb{C}, \; \text{HasStrictDerivAt}(\sin, \cos x, x). $$$$

Lean4

/-- The complex sine function is everywhere strictly differentiable, with the derivative `cos x`. -/
theorem hasStrictDerivAt_sin (x : ℂ) : HasStrictDerivAt sin (cos x) x :=
  by
  simp only [cos, div_eq_mul_inv]
  convert
    ((((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp.sub ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
          I).mul_const
      (2 : ℂ)⁻¹ using
    1
  simp only [id]
  rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc, I_mul_I, mul_neg_one,
    sub_neg_eq_add, add_comm]

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