euler_sineTerm_tprod — Mathlib

English

For x not an integer, the infinite product over sineTerm equals sin(π x)/(π x).

Русский

Для x, не целого, бесконечный произведение по sineTerm равно sin(π x)/(π x).

LaTeX

$$$$\prod_{i=0}^{\infty} (1 + \text{sineTerm}(x, i)) = \frac{\sin(\pi x)}{\pi x} \quad (x \notin \mathbb{Z}). $$$$

Lean4

theorem euler_sineTerm_tprod (hx : x ∈ ℂ_ℤ) : ∏' i : ℕ, (1 + sineTerm x i) = Complex.sin (π * x) / (π * x) :=
  by
  rw [← Multipliable.hasProd_iff (multipliable_sineTerm x),
    Multipliable.hasProd_iff_tendsto_nat (multipliable_sineTerm x)]
  exact tendsto_euler_sin_prod' (integerComplement.ne_zero hx)

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