antideriv_sin_comp_const_mul — Mathlib

English

For hz ≠ 0 and x ∈ ℝ, the derivative of y ↦ -cos(2 z y)/(2 z) at y = x is sin(2 z x).

Русский

При z ≠ 0 и x ∈ ℝ производная функции y ↦ -cos(2 z y)/(2 z) в точке y = x равна sin(2 z x).

LaTeX

$$$\frac{d}{dy}\Big|_{y=x} \Big(-\frac{\cos(2 z y)}{2 z}\Big) = \sin(2 z x)$$$

Lean4

theorem antideriv_sin_comp_const_mul (hz : z ≠ 0) (x : ℝ) :
    HasDerivAt (fun y : ℝ => -Complex.cos (2 * z * y) / (2 * z)) (Complex.sin (2 * z * x)) x :=
  by
  have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
  have b : HasDerivAt (Complex.cos ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_cos (x * (2 * z))) a
  have c := (b.comp_ofReal.div_const (2 * z)).fun_neg
  simp at c ⊢; field_simp at c ⊢; simp only [mul_rotate _ 2 z] at c
  exact c

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