multipliable_sineTerm

Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

← MathLib Explorer

English

See item 61150 for the q-expansion of π cot(π z).

Русский

См. пункт 61150 для расширенного ряда π cot(π z).

LaTeX

$$$$\text{(dup) } \pi \cot(\pi z) = \pi i - 2\pi i \sum_{n \ge 0} e^{2\pi i z n}. $$$$

Lean4

theorem multipliable_sineTerm (x : ℂ) : Multipliable fun i ↦ (1 + sineTerm x i) :=
  by
  apply multipliable_one_add_of_summable
  have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two
  simpa [sineTerm] using this

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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