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.
• cos_le_sinc: cos x ≤ sinc x for |x| < π / 2, which together with sinc_le_one gives the squeeze behind the limit of sin x / x at 0.
• sinc_pos: sinc is positive on (-π, π).

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

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

Equations

• Real.sinc x = if x = 0 then 1 else Real.sin x / x

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.

theorem Real.cos_le_sinc {x : ℝ} (hx : |x| < Real.pi / 2) : cos x ≤ sinc x

For |x| < π / 2 we have cos x ≤ sinc x, and together with sinc_le_one this gives the squeeze cos x ≤ sin x / x ≤ 1.

theorem Real.sinc_pos {x : ℝ} (hx : |x| < Real.pi) : 0 < sinc x

The function sinc is positive on (-π, π).