English
The tendsto of Euler sine product to the ratio sin(π x)/(π x) for x ≠ integer.
Русский
Предел бесконечного произведения Эйлера к отношению sin(π x)/(π x) при x ≠ целое.
LaTeX
$$$$\forall x \in \mathbb{C}, x \notin \mathbb{Z}, \; \mathrm{Tendsto}\big( n \mapsto \prod_{i=0}^{n-1} (1 + \text{sineTerm}(x,i)) \big) \to \frac{\sin(\pi x)}{\pi x}.$$$$
Lean4
theorem tendsto_logDeriv_euler_sin_div (hx : x ∈ ℂ_ℤ) :
Tendsto (fun n : ℕ ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
(𝓝 <| logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x) :=
by
refine
logDeriv_tendsto (isOpen_compl_range_intCast) ⟨x, hx⟩
HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
· filter_upwards with n using by fun_prop
· simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩
