integrable_sinc — Mathlib

English

The sinc function is integrable with respect to any finite measure on ℝ.

Русский

Функция sinc интегрируема относительно любой конечной меры на ℝ.

LaTeX

$$$ \\text{Integrable}(\\text{Real}.sinc)\\ μ $$$

Lean4

@[fun_prop]
theorem integrable_sinc {μ : Measure ℝ} [IsFiniteMeasure μ] : Integrable sinc μ :=
  by
  refine Integrable.mono' (g := fun _ ↦ 1) (by fun_prop) (by fun_prop) <| ae_of_all _ fun x ↦ ?_
  rw [Real.norm_eq_abs]
  exact abs_sinc_le_one x

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