sinc — Mathlib

English

The sinc function is defined by sinc(x) = 1 if x = 0, and sinc(x) = sin x / x otherwise.

Русский

Функция sinc задаётся как sinc(x) = 1 при x = 0, и sinc(x) = sin x / x иначе.

LaTeX

$$$\\operatorname{sinc}(x) = \begin{cases}1, & x=0 \\[2mm] \\frac{\sin x}{x}, & x\neq 0\end{cases}$$$

Lean4

/-- The function `sin x / x` modified to take the value 1 at 0, which makes it continuous. -/
@[pp_nodot]
noncomputable def sinc (x : ℝ) : ℝ :=
  if x = 0 then 1 else sin x / x

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