sinKernel_undef

Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

URI: https://scilib.ai/kg/mathlib#HurwitzZeta.sinKernel_undef

← MathLib Explorer

English

If a ∈ UnitAddCircle and x ≤ 0, then sinKernel(a)(x) = 0.

Русский

Если a ∈ UnitAddCircle и x ≤ 0, то sinKernel(a)(x) = 0.

LaTeX

$$$$\\text{If } x \\le 0, \\ \\text{sinKernel}(a,x) = 0. $$$$

Lean4

theorem sinKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : sinKernel a x = 0 := by
  induction a using QuotientAddGroup.induction_on with
  | H a => rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]

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

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

Разделы

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

Аффилиация

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