r

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

URI: https://scilib.ai/kg/mathlib#EisensteinSeries.r

← MathLib Explorer

English

The function r is defined by r(z) = min(z.im, sqrt(r1(z))).

Русский

Функция r определяется как r(z) = min(z.im, sqrt(r1(z))).

LaTeX

$$$ r(z) = \\min\\left(\\operatorname{Im} z, \\sqrt{r_1(z)}\\right)$$$

Lean4

/-- This function is used to give an upper bound on the summands in Eisenstein series; it is
defined by `z ↦ min z.im √(z.im ^ 2 / (z.re ^ 2 + z.im ^ 2))`. -/
def r : ℝ :=
  min z.im √(r1 z)

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

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

Разделы

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

Аффилиация

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