integral_exp_mul_I_eq_sin — Mathlib

English

For real r, the integral ∫_{-r}^r exp(i t) dt equals 2 sin r.

Русский

Пусть r ∈ ℝ. Тогда ∫_{-r}^r e^{i t} dt = 2 sin r.

LaTeX

$$$\forall r \in \mathbb{R},\ \displaystyle \int_{-r}^r e^{i t} \, dt = 2 \sin r$$$

Lean4

theorem integral_exp_mul_I_eq_sin (r : ℝ) : ∫ t in -r..r, Complex.exp (t * Complex.I) = 2 * Real.sin r :=
  calc
    ∫ t in -r..r, Complex.exp (t * Complex.I)
    _ = (Complex.exp (Complex.I * r) - Complex.exp (Complex.I * (-r))) / Complex.I :=
      by
      simp_rw [mul_comm _ Complex.I]
      rw [integral_exp_mul_complex]
      · simp
      · simp
    _ = 2 * Real.sin r :=
      by
      simp only [mul_comm Complex.I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg, add_sub_add_left_eq_sub,
        Complex.div_I, Complex.ofReal_sin]
      rw [sub_mul, mul_assoc, mul_assoc, two_mul]
      simp

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