r1 — Mathlib · SciLib

English

Define a real-valued auxiliary function on the upper half-plane by r1(z) = (Im z)^2 / (Re z^2 + Im z^2).

Русский

Введем вспомогательную функцию r1 на верхней полуплоскости: r1(z) = (Im z)^2 / ((Re z)^2 + (Im z)^2).

LaTeX

$$$r_1(z) = \dfrac{\operatorname{Im}(z)^2}{\operatorname{Re}(z)^2 + \operatorname{Im}(z)^2}$$$

Lean4

/-- Auxiliary function used for bounding Eisenstein series, defined as
  `z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)`. -/
def r1 : ℝ :=
  z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)

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