partitions-leanblueprint
0.1 Definitions
In lean, A modular form of weight \(k \in \mathbb {N}\) is a function \(f : \mathbb {C} → \mathbb {C}\) such that :
(1) \(f\) is holomorphic on \(\mathbb {H}\)
(2) For all \(z \in \mathbb {H}, f(z + 1) = f(z)\)
(3) For all \(z \in \mathbb {H}, f(-1/z) = z^{k} f(z)\)
(4) \(f\) is bounded as Im\((z) \to \infty \)
An integer modular form of weight \(k \in \mathbb {N}\) is a sequence \(a : \mathbb {N} → \mathbb {Z}\) such that \(\sum _{n=0}^{\infty } a(n) q^n\) is a modular form of weight \(k\), where \(q = e ^{2 \pi i z}.\)
A modular form mod \(\ell \) of weight \(k \in \mathbb {Z} / (\ell - 1) \mathbb {Z}\) is a sequence \(a : \mathbb {N} → \mathbb {Z} / \ell \mathbb {Z}\) such that there exists an integer modular form \(b\) of weight \(k'\) where \(b \equiv a \mod \ell \) and \(k' \equiv k \mod (\ell - 1)\).
\(\Theta \) sends modular forms mod \(\ell \) of weight \(k\) to weight \(k + 2\) by
\((\Theta a) n = n a(n).\)
The operator \(U\) sends modular forms mod \(\ell \) of weight \(k\) to weight \(k\) by
\( (a|U) n = a(\ell n).\)
A modular form mod \(\ell \) called \(a\) has weight \(j \in \mathbb {N}\) if there exists an integer modular form \(b\) of weight \(j\) such that \(b \equiv a \mod \ell \).
Let a be a of a modular form mod \(\ell \). The filtration of \(a, \omega (a), \) is defined as the minimum natural number \(j\) such that \(a\) has weight \(j\). The filtration of the zero function is \(0\).
It’s worth stated how multiplication and exponentiation are defined here, because they are not defined in the normal way. The multiplication of two modular forms mod \(\ell \) called \(a\) and \(b\) is defined as
The exponentiation of a modular form mod \(\ell \) called \(a\) to the power of \(j \in \mathbb {N}\) is defined as
0.2 PowPrime
Two functions \(a, b : \) Fin \(n \to \mathbb {N}\), which can be thought of as tuples of n natural numbers, are permutationally equivalent if there exists a bijective function \(\sigma : \) Fin \(n \to \) Fin \(n\) such that \(a = b \circ \sigma \). This is an equivalence relation.
If \(x = (x_1, x_2, ..., x_k)\) is not constant (i.e not all \(x_i\) are equal) then for any \(n \in \mathbb {N}\),
If \(x\) and \(y\) are permutationally equivalent then \(\prod _{i = 1}^k a(x_i) = \prod _{i = 1}^k a(y_i)\).
Let \(x = (x_1, x_2, ..., x_k)\) and \(n \in \mathbb {N}\). Suppose that \(\sum _{i = 1}^k x_i = n\).
(1) If \(k \nmid n\) then \(x\) is not constant.
(2) If \(k \mid n\) and \(x \neq (n/k, ..., n/k)\) then \(x\) is not constant.
Let \(\ell \) be a prime and \(a\) a modular form mod \(\ell \) of any weight. Then
0.3 Theorems
Let \(a\) be a modular form mod \(\ell \). Then \((a|U) ^\ell = a - \Theta ^{\ell - 1} a\).
Let a be a modular form mod \(\ell \). If \(\omega (a) = 0\) then \(a\) is constant, i.e. for all \(n {\gt} 0, a(n) = 0\).
Let a be a modular form mod \(\ell \) and \(i \in \mathbb {N}\). Then \(\omega (a ^i)\) = \(i \omega (a)\).
\(\Delta \) is the sequence obtained from \(q (\prod _{n = 1}^{\infty } (1 - q^n))^{24}\). It is a modular form mod \(\ell \) of weight \(12\).
For a prime \(\ell \ge 5\), we define \(\delta _\ell = \frac{\ell ^2 - 1}{24} \in \mathbb {N}\). We define \(f_\ell = \Delta ^{\delta _\ell }\), which is a modular form mod \(\ell \) of weight \(12 \delta _\ell \).
\( \omega (f_\ell ) = 12 \delta _\ell = \frac{\ell ^2 - 1}{2}.\)
This is part (1) of Lemma 2.1.
Let \(a\) be a modular form mod \(\ell \). Then \(\omega (\Theta a) \le \omega (a) + \ell + 1\).
This is part (2) of Lemma 2.1.
Let \(a\) be a modular form mod \(\ell \). Then \(\omega (\Theta a) = \omega (a) + \ell + 1\) if and only if \(\ell \nmid \omega (a).\)
This is Lemma 3.2.
For all \(m \in \mathbb {N}\), \(\omega (\Theta ^m f_\ell ) \ge \omega (f_\ell ) = \frac{\ell ^2 - 1}{2}.\)
This is part (1) of Lemma 3.3.
If \(\ell \nmid \omega (\Theta ^{\ell - 1} f_\ell )\) then \(\omega (\Theta ^{\ell - 1} f_\ell ) = \frac{\ell ^2 - 1}{2}.\)
This is part (2) of Lemma 3.3.
If \(\ell \mid \omega (\Theta ^{\ell - 1} f_\ell )\) then \(\omega (f_\ell | U) {\gt} 0\).