integral_exp_mul_I_eq_sinc — Mathlib

English

For real r, ∫_{-r}^r exp(i t) dt equals 2 r sinc r, where sinc r = sin r / r.

Русский

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

LaTeX

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

Lean4

theorem integral_exp_mul_I_eq_sinc (r : ℝ) : ∫ t in -r..r, Complex.exp (t * Complex.I) = 2 * r * sinc r :=
  by
  rw [integral_exp_mul_I_eq_sin]
  by_cases hr : r = 0
  · simp [hr]
  rw [sinc_of_ne_zero hr]
  norm_cast
  field_simp

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