cosKernel_def

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

← MathLib Explorer

English

For a = 0, the two kernels coincide: evenKernel 0 = cosKernel 0.

Русский

Для a = 0 две ядра совпадают: evenKernel 0 = cosKernel 0.

LaTeX

$$$$\\operatorname{evenKernel}(0,x) = \\operatorname{cosKernel}(0,x).$$$$

Lean4

theorem cosKernel_def (a x : ℝ) : ↑(cosKernel (↑a) x) = jacobiTheta₂ a (I * x) := by
  simp [cosKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two, mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

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

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

Разделы

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

Аффилиация

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