antideriv_cos_comp_const_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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