Sinc function

This file contains the definition of the sinc function and some of its properties.

Main definitions

• Real.sinc: the (unnormalized) sinc function, defined as sinc x = sin x / x for x ≠ 0 and 1 for x = 0.

Main statements

• continuous_sinc: the sinc function is continuous.

noncomputable def Real.sinc (x : ℝ) : ℝ

The function sin x / x modified to take the value 1 at 0, which makes it continuous.

theorem Real.sinc_apply {x : ℝ} : sinc x = if x = 0 then 1 else sin x / x

@[simp]

theorem Real.sinc_zero : sinc 0 = 1

theorem Real.sinc_of_ne_zero {x : ℝ} (hx : x ≠ 0) : sinc x = sin x / x

theorem Real.sinc_eq_dslope : sinc = dslope sin 0

@[simp]

theorem Real.sinc_neg (x : ℝ) : sinc (-x) = sinc x

theorem Real.abs_sinc_le_one (x : ℝ) : |sinc x| ≤ 1

theorem Real.sinc_le_one (x : ℝ) : sinc x ≤ 1

theorem Real.neg_one_le_sinc (x : ℝ) : -1 ≤ sinc x

theorem Real.sin_div_le_inv_abs (x : ℝ) : sin x / x ≤ |x|⁻¹

theorem Real.sinc_le_inv_abs {x : ℝ} (hx : x ≠ 0) : sinc x ≤ |x|⁻¹

theorem Real.continuous_sinc : Continuous sinc

The function sinc is continuous.