Differentiability of sinc and dslope

This file proves that the sinc function is differentiable everywhere, including at 0.

Main results

• Real.differentiableAt_sinc: sinc is differentiable at every point
• Real.hasDerivAt_sinc_zero: sinc has derivative 0 at x = 0

Mathematical background

The sinc function is defined as:

• sinc x = sin x / x for x ≠ 0
• sinc 0 = 1

Equivalently, sinc = dslope sin 0.

The derivative of sinc at 0 can be computed using Taylor expansion:

• sin x = x - x³/6 + x⁵/120 - ...
• sinc x = 1 - x²/6 + x⁴/120 - ...
• sinc'(0) = 0

theorem Real.abs_sin_sub_self_le (x : ℝ) (hx : |x| ≤ 1) : |sin x - x| ≤ |x| ^ 3 / 4

Bound on |sin x - x| in terms of |x|³. For x > 0: sin x < x and x - x³/4 < sin x, so 0 < x - sin x < x³/4. By symmetry (sin(-x) = -sin(x)), |sin x - x| ≤ |x|³/4 for all x with |x| ≤ 1.

theorem Real.hasDerivAt_sinc_zero : HasDerivAt sinc 0 0

The derivative of sinc at 0 is 0.

The proof uses the squeeze theorem with the bound |sinc x - 1| ≤ |x|² / 4, which follows from sin bounds in Mathlib.

theorem Real.differentiableAt_sinc_zero : DifferentiableAt ℝ sinc 0

theorem Real.differentiableAt_sinc (x : ℝ) : DifferentiableAt ℝ sinc x

sinc is differentiable everywhere.

theorem Real.differentiable_sinc : Differentiable ℝ sinc

sinc is a differentiable function.

theorem Real.sinc_eq_integral_cos (x : ℝ) : sinc x = ∫ (t : ℝ) in 0..1, cos (x * t)

Integral representation of sinc: sinc x = ∫ t in 0..1, cos (x * t). This is the standard average-cosine form used for derivative bounds.

theorem Real.hasDerivAt_sinc_of_ne_zero {x : ℝ} (hx : x ≠ 0) : HasDerivAt sinc ((x * cos x - sin x) / x ^ 2) x

The derivative of sinc at a nonzero point.

theorem Real.deriv_sinc {x : ℝ} : deriv sinc x = if x = 0 then 0 else (x * cos x - sin x) / x ^ 2

The derivative of sinc. For x = 0, deriv sinc 0 = 0. For x ≠ 0, deriv sinc x = (x cos x - sin x) / x².

@[simp]

theorem Real.deriv_sinc_zero : deriv sinc 0 = 0

theorem Real.abs_x_mul_cos_sub_sin_le_sq (x : ℝ) : |x * cos x - sin x| ≤ x ^ 2

Bound: |x cos x - sin x| ≤ x² for all x. Proof uses monotonicity of auxiliary functions on [0, ∞).

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

theorem Real.deriv_sinc_mem_Icc (x : ℝ) : deriv sinc x ∈ Set.Icc (-1) 1

deriv sinc x is in [-1, 1] for all x

Integral representation and smoothness of sinc

The sinc function is smooth (C^∞). The key insight is the integral representation: sinc(x) = ∫ t in 0..1, cos(t * x) dt

This works because:

• For x ≠ 0: ∫₀¹ cos(tx) dt = [sin(tx)/x]₀¹ = sin(x)/x = sinc(x)
• For x = 0: ∫₀¹ cos(0) dt = ∫₀¹ 1 dt = 1 = sinc(0)

Smoothness follows from differentiation under the integral sign (Leibniz rule): since cos(t*x) is C^∞ in x and the domain [0,1] is compact, the integral is C^∞.

theorem Real.sinc_eq_integral (x : ℝ) : sinc x = ∫ (t : ℝ) in 0..1, cos (t * x)

The integral representation of sinc: sinc(x) = ∫ t in 0..1, cos(t * x)

theorem Real.deriv_sinc_eq_dslope : deriv sinc = dslope (cos - sinc) 0

The derivative of sinc equals dslope (cos - sinc) at 0.

For x ≠ 0: dslope (cos - sinc) 0 x = (cos x - sinc x) / x = (x cos x - sin x) / x² = deriv sinc x

For x = 0: dslope (cos - sinc) 0 0 = deriv (cos - sinc) 0 = -sin 0 - deriv sinc 0 = 0 = deriv sinc 0

theorem Real.contDiffAt_sinc_of_ne_zero {x : ℝ} (hx : x ≠ 0) : ContDiffAt ℝ ⊤ sinc x

sinc is smooth at every nonzero point.

theorem Real.analyticAt_sinc_zero : AnalyticAt ℝ sinc 0

sinc is analytic at 0.

The proof uses the order theory of analytic functions. Since sin is analytic at 0 with order ≥ 1 (because sin(0) = 0), there exists an analytic function g such that sin(z) = z • g(z) near 0. This g must equal sinc away from 0, and by continuity of both functions at 0, g = sinc everywhere near 0. Therefore sinc is analytic at 0.

theorem Real.analyticAt_sinc (x : ℝ) : AnalyticAt ℝ sinc x

sinc is analytic at every point.

theorem Real.contDiff_sinc : ContDiff ℝ ⊤ sinc

sinc is smooth (infinitely differentiable).

The proof uses that sinc is analytic everywhere (analyticAt_sinc), and analytic functions are smooth.

theorem Real.analyticOnNhd_sinc : AnalyticOnNhd ℝ sinc Set.univ

sinc is an analytic function.