HasProdUniformlyOn_sineTerm_prod_on_compact

English

There exists HasProdUniformlyOn for the product with sineTerm over a compact Z, equating to the sine/cotangent expression.

Русский

Существует HasProdUniformlyOn для произведения с sineTerm над компактным Z, равное выражению через синус и котангенс.

LaTeX

$$$$\text{HasProdUniformlyOn}(\lambda n z. 1 + \text{sineTerm}(z, n), \text{cotTerm}(x, j)\,|\, Z).$$$$

Lean4

theorem HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ) (hZC : IsCompact Z) :
    HasProdUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) (fun x => (Complex.sin (↑π * x) / (↑π * x)))
      { Z } :=
  by
  apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right
  exact fun s hs x hx => euler_sineTerm_tprod (by aesop)

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