sineTerm

Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

URI: https://scilib.ai/kg/mathlib#sineTerm

English

The main term in the Weierstrass product for sine is defined as sineTerm(x, n) = - x^2 /(n+1)^2.

Русский

Основной член произведения для синуса задаётся как sineTerm(x, n) = -x^2/(n+1)^2.

LaTeX

$$$$\text{sineTerm}(x, n) = -\frac{x^2}{(n+1)^2}.$$$$

Lean4

/-- The main term in the infinite product for sine. -/
noncomputable abbrev sineTerm (x : ℂ) (n : ℕ) : ℂ :=
  -x ^ 2 / (n + 1) ^ 2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru