Assumptions:
TeX:
E_{2 k}\!\left(i \infty\right) = \lim_{\tau \to i \infty} E_{2 k}\!\left(\tau\right) = 1
k \in \mathbb{Z}_{\ge 1}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| EisensteinE | Normalized Eisenstein series | |
| ConstI | Imaginary unit | |
| Infinity | Positive infinity | |
| ComplexLimit | Limiting value, complex variable | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("ad9ba2"),
Formula(Equal(EisensteinE(Mul(2, k), Mul(ConstI, Infinity)), ComplexLimit(EisensteinE(Mul(2, k), tau), For(tau, Mul(ConstI, Infinity))), 1)),
Variables(k),
Assumptions(And(Element(k, ZZGreaterEqual(1)))))