Follows from the definition of the slash operator: (F|_{k}(-I))(z) = (-1)^{-k}F((-I)z) = F(z).

This follows from the fact that the sum converges absolutely. Applying the slash operator with \gamma = \left(\begin{smallmatrix} 0 & -1 \\ 1 & 0 \end{smallmatrix}\right) gives eqn:Ek-trans-S.

Note that the assumption on polynomial growth holds when f is a holomorphic modular form, where the proof can be found in Serre (1973) for the case of level-one modular forms. This has been done in Lean 4 by David Loeffler.

This is exercise 1.2.8 of Diamond and Shurman (2005).

Use the fact that \mathrm{SL}_2(\mathbb{Z}) is generated by S and T. Then eqn:E2-transform-general follows from eqn:E2-S-transform together with E_2|_T = E_2.

Consider the logarithmic derivative of \eta, which is equal to \frac{\pi i}{12} E_2. The result then follows from the transformation of E_2. See Diamond and Shurman (2005), Proposition 1.2.5.

The fact that it is invariant under translation is clear from the definition, so we only need to check transformation under S. Now, note that \eta^{24} = \Delta, and from Lemma 7.21 we have \eta(-1/z) = \sqrt{-iz} \eta(z), so \Delta(-1/z) = z^{12} \Delta(z) as required.

We only need to show its a cuspform, since once we have this, dividing the rhs by \Delta would give a modular form of weight 0 which is a constant, and so we can determine the constant easily. /- source paragraph break -/ To check its a cuspform, we just look at the q-expansions of E_4 and E_6 and prove directly that the first term vanishes.

By Definition 7.22, \Delta(it) = e^{-2 \pi t} \prod_{n \ge 1} (1 - e^{-2 \pi n t})^{24} > 0.

This follows from the product formula.

The proof makes use of the maximum modulus principle. Since this is already formalized, we skip the details here, but see the Lean proof for them.

First we note that for 2 < k we have \dim(M_k(\Gamma_1)) = 1 + \dim S_k(\Gamma_1). This follows since we know the E_k are in M_k so by scaling appropriately, any non-cuspform f \in M_k we would have f - aE_k \in S_k for some a. /- source paragraph break -/ Next, note that S_k(\Gamma_1) is isomorphic to M_{k-12}(\Gamma_1), since if f \in S_k then f/\Delta is now a modular form (using the product expansion of \Delta and its non-vanishing on \mathfrak{H}) of weight k-12. Note its important that f is a cuspform so that the quotient by \Delta is a modular form. /- source paragraph break -/ So we only need to know the dimensions of M_k(\Gamma_1) for 0 \le k \le 12. For k = 0 we have \dim M_0(\Gamma_1) = 1 by Theorem 7.27. For k = 4 we have \dim M_4(\Gamma_1) = 1 since if there was a cuspform f of weight 4 then f/\Delta would be a modular form of negative weight, i.e. zero, so f=0. Similarly for k=6,8,10. For k=12 we have \dim S_{12}(\Gamma_1) = 1 since the discriminant form is a cusp form of weight 12 and any other cusp form of weight 12 would be a scalar multiple of \Delta (since their ratio would be a modular form of weight 0). So we have \dim M_{12}(\Gamma_1) = 2. /- source paragraph break -/ Finally we need to check that \dim M_2(\Gamma_1) = 0. Firstly, there can't be any cuspforms here by the same argument as above. So we need to check that there are no modular forms of weight 2. If we did have one, call it f then f^2 would be a non-cuspform of weight 4 and so f^2 = a E_4, where in fact a=a_0(f)^2 (since (f^2-a_0(f)E_4) is now a cuspform of weight 4 which means its zero). Similarly, f^3 = a_0(f)^3 E_6. But now taking powers to make them weight 12 forms we see that a_0(f)^6(E_4^3 - E_6^2) = 0 = 1728 a_0(f)^6 \Delta, but a_0(f) \ne 0 (since its assumed to not be a cuspform), this would mean \Delta =0 which we know can't happen.

We know that \dim(M_k(\Gamma_1)) is finite-dimensional, hence there is some r_k such that any element of M_k(\Gamma_1) vanishing at infinity to degree greater than r_k must be zero. Now take f \in M_k(\Gamma) vanishing to degree n at infinity, and set F = \prod_\gamma f\mid_k \gamma, where the product is over a set of representatives of \Gamma_1 \backslash \Gamma. Then F is a modular form of weight kd where d = [\Gamma_1 : \Gamma], and it vanishes at infinity to degree at least n. So if n > r_{kd}, then F=0, and hence f=0.