HasProdLocallyUniformlyOn_euler_sin_prod

English

There is HasProdLocallyUniformlyOn for the euler sine product on the complex integers ℂ_ℤ.

Русский

Существуют локальные равномерные произведения для эйлерова синус-произведения на ℂ_ℤ.

LaTeX

$$$$\text{HasProdLocallyUniformlyOn}(\lambda n z. 1 + \text{sineTerm}(z, n), \mathbb{C}_{\mathbb{Z}}).$$$$

Lean4

theorem HasProdLocallyUniformlyOn_euler_sin_prod :
    HasProdLocallyUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) (fun x => (Complex.sin (π * x) / (π * x)))
      ℂ_ℤ :=
  by
  apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_compl_range_intCast
  exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC

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