English
For nonzero z ∈ ℂ and a,b ∈ ℝ, ∫_a^b cos(z x) dx = (sin(z b) − sin(z a))/z.
Русский
Для z ∈ ℂ, z ≠ 0, и a,b ∈ ℝ, ∫_a^b cos(z x) dx = (sin(z b) − sin(z a))/z.
LaTeX
$$$\forall z \in \mathbb{C},\ z \neq 0,\ \forall a,b \in \mathbb{R},\displaystyle \int_a^b \cos(z x) \, dx = \frac{\sin(z b) - \sin(z a)}{z}$$$
Lean4
theorem integral_cos_mul_complex {z : ℂ} (hz : z ≠ 0) (a b : ℝ) :
(∫ x in a..b, Complex.cos (z * x)) = Complex.sin (z * b) / z - Complex.sin (z * a) / z :=
by
apply integral_eq_sub_of_hasDerivAt
swap
· apply Continuous.intervalIntegrable
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)
intro x _
have a := Complex.hasDerivAt_sin (↑x * z)
have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
have d := HasDerivAt.comp_ofReal (c.div_const z)
simp only [mul_comm] at d
convert d using 1
conv_rhs => arg 1; rw [mul_comm]
rw [mul_div_cancel_right₀ _ hz]
