sinc_neg — Mathlib

English

Let sinc denote the normalized sinc function on the real line. Then sinc is an even function: sinc(-x) = sinc(x) for all real x.

Русский

Пусть sinc обозначает нормализованную функцию sinc на ℝ. Тогда она чётна: sinc(-x) = sinc(x) для всех x ∈ ℝ.

LaTeX

$$$\operatorname{sinc}(-x) = \operatorname{sinc}(x)$$$

Lean4

@[simp]
theorem sinc_neg (x : ℝ) : sinc (-x) = sinc x := by
  by_cases hx : x = 0
  · simp [hx]
  · simp [sinc_of_ne_zero hx, sinc_of_ne_zero (neg_ne_zero.mpr hx)]

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