- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
We have
There exists a constant \(C_0 {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
We have
There exists a constant \(C_{-2} {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
There exists a constant \(C_{-4} {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
We have
All three functions \(t \mapsto H_2(it), H_3(it), H_4(it)\) are positive for \(t {\gt} 0\).
All packing \(\mathcal{P} \subseteq \mathbb {R}^8\) has density satisfying \(\Delta _{\mathcal{P}} \leq \Delta _{E_8}\).
For \(x\in \mathbb {R}^8\) we define
For \(x\in \mathbb {R}^8\) define
A subgroup \(\Gamma \subset \Gamma _1\) is called a congruence subgroup if \(\Gamma (N)\subset \Gamma \) for some \(N\in \mathbb {N}\).
Define two (quasi) modular forms as
The Fourier transform of an \(L^1\)-function \(f:\mathbb {R}^d\to \mathbb {C}\) is defined as
where \(\langle x, y \rangle = \frac12\| x\| ^2 + \frac12\| y\| ^2 - \frac12\| x - y\| ^2\) is the standard scalar product in \(\mathbb {R}^d\).
The modular group \(\Gamma _1:=\mathrm{SL}_2(\mathbb {Z})\) acts on \(\mathfrak {H}\) by linear fractional transformations
Define the matrices
It is easily verifiable that \(\alpha = T^2\) and \(\beta = -S\alpha ^{-1}S = -ST^{-2}S\).
Define
Let \(\Gamma \) denote a subgroup of \(\mathrm{SL}_2(\mathbb {Z})\), then a modular form of level \(\Gamma \) and weight \(k \in \mathbb {Z}\) is a function \(f : \mathbb {H} \to \mathbb {C}\) such that:
For all \(\gamma \in \Gamma \) we have \(f\mid _k \gamma = f\) (such functions are called slash invariant).
\(f\) is holomorphic on \(\mathbb {H}\).
For all \(\gamma \in \mathrm{SL}_2(\mathbb {Z})\), there exist \(A, B \in \mathbb {R}\) such that for all \(z \in \mathbb {H}\), with \( A \le \mathrm{Im}(z)\), we have \(|(f \mid _k \gamma ) (z) |\le B\). Here \(| - |\) denotes the standard complex absolute value.
The level \(N\) principal congruence subgroup of \(\Gamma _1\) is
The periodic sphere packing constant is defined to be
We define the following three functions
A \(C^\infty \) function \(f:\mathbb {R}^d\to \mathbb {C}\) is called a Schwartz function if it decays to zero as \(\| x\| \to \infty \) faster then any inverse power of \(\| x\| \), and the same holds for all partial derivatives of \(f\), ie, if for all \(k, n \in \mathbb {N}\), there exists a constant \(C \in \mathbb {R}\) such that for all \(x \in \mathbb {R}^d\), \(\left\lVert x \right\rVert ^k \cdot \left\lVert f^{(n)}(x) \right\rVert \leq C\), where \(f^{(n)}\) denotes the \(n\)-th derivative of \(f\) considered along with the appropriate operator norm. The set of all Schwartz functions from \(\mathbb {R}^d\) to \(\mathbb {C}\) is called the Schwartz space. It is an \(\mathbb {R}\)-vector space.
Let \(F\) be a function on \(\mathfrak {H}\) and \(\gamma \in \mathrm{SL}_2(\mathbb {Z})\). Then the slash operator acts on \(F\) by
We define three different theta functions (so called “Thetanullwerte”) as
(\(E_8\)-lattice, Definition 2)We define the \(E_8\) basis vectors to be the set of vectors
More explicitly, we have
We have an equality of operators \(D = q \frac{\mathrm{d}}{\mathrm{d}q}\). In particular, the \(q\)-series of the derivative of a quasimodular form \(F(z) = \sum _{n \ge n_0} a_n q^n\) is \(F'(z) = \sum _{n \ge n_0} n a_n q^n\).
The Eisenstein series possesses the Fourier expansion
where \(\sigma _{k-1}(n)\, =\, \sum _{d|n} d^{k-1}\). In particular, we have
\(F\) and \(G\) satisfy the following differential equations:
We have
Let \(X \subset \mathbb {R}^d\) be a set of sphere packing centres of separation \(1\) that is periodic with some lattice \(\Lambda \subset \mathbb {R}^d\). Then, there exists \(k \in \mathbb {N}\) sufficiently large such that
These three theta functions satisfy the Jacobi identity
For all \(R\), we have the following inequality relating the number of lattice points from \(\Lambda \) in a ball with the volume of the ball and the fundamental region \(\mathcal{D}\):
We have
Let \(f(z)\) be a holomorphic function with a Fourier expansion
with \(c_f(n_0) \ne 0\). Assume that \(c_f(n)\) has a polynomial growth, i.e. \(|c_f(n)| = O(n^k)\) for some \(k \in \mathbb {N}\). Then there exists a constant \(C_f {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
: Let \(\Gamma \) be a finite index subgroup of \(\mathrm{SL}_2(\mathbb {Z})\) and \(f \in \mathcal{M}_k(\Gamma )\) be a modular form of weight \(k\). Then the Fourier coefficients \(a_n(f)\) has a polynomial growth, i.e. \(|a_n(f)| = O(n^k)\).
For all \(R\), we have the following inequality relating the number of points from \(X\) (periodic w.r.t. \(\Lambda \)) in a ball with the number of points from \(\Lambda \):
We have
There exists a constant \(C_I {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
The Fourier expansions of these functions are
There exists a constant \(C_S {\gt} 0\) such that
for all \(z\) with \(\Im z {\gt} 1/2\).
\(\psi _S(z)\) can be written as
We have
Let \(f : \mathbb {R}^d \to \mathbb {C}\) be a Schwartz function and let \(X \subset \mathbb {R}^d\) be periodic with respect to some lattice \(\Lambda \subset \mathbb {R}^d\). Then,
For any \(R {\gt} 0\),
These elements act on the theta functions in the following way
and
For \(r\geq 0\) we have
The integral converges absolutely for all \(r\in \mathbb {R}_{\geq 0}\).
For \(r{\gt}\sqrt{2}\) we can express \(a(r)\) in the following form
For \(r\geq 0\) we have
The integral converges absolutely for all \(r\in \mathbb {R}_{\geq 0}\).
For \(r{\gt}\sqrt{2}\) function \(b(r)\) can be expressed as
\(H_2\) admits a Fourier series of the form
for some \(c_{H_2}(n) \in \mathbb {R}_{\ge 0}\), with \(c_{H_2}(1) = 16\) and \(c_{H_2}(n) = O(n^k)\) for some \(k \in \mathbb {N}\).
\(H_3\) admits a Fourier series of the form
for some \(c_{H_3}(n) \in \mathbb {R}_{\ge 0}\) with \(c_{H_3}(0) = 1\) and \(c_{H_3}(n) = O(n^k)\) for some \(k \in \mathbb {N}\). Especially, \(H_3\) is not cuspidal.
\(H_4\) admits a Fourier series of the form
for some \(c_{H_4}(n) \in \mathbb {R}\) with \(c_{H_4}(0) = 1\) and \(c_{H_4}(n) = O(n^k)\) for some \(k \in \mathbb {N}\). Especially, \(H_4\) is not cuspidal.
Consider the function \(A:(0,\infty )\to \mathbb {C}\) defined as
Then
for all \(t {\gt} 0\).
Consider the function \(B:(0,\infty )\to \mathbb {C}\) defined as
Then
for all \(t {\gt} 0\).
We have
or equivalently,
Given a set \(X \subset \mathbb {R}^d\) and a real number \(r {\gt} 0\) (known as the separation radius) such that \(\| x - y\| \geq r\) for all distinct \(x, y \in X\), we define the sphere packing \(\mathcal{P}(X)\) with centres at \(X\) to be the union of all open balls of radius \(r\) centred at points in \(X\):
Given a sphere packing \(\mathcal{P}(X)\) with separation radius \(r\), we defined the scaled packing with respect to a real number \(c {\gt} 0\) to be the packing \(\mathcal{P}(cX)\), where \(cX = \left\{ cx \in V \; \middle | \; x \in X \right\} \) has separation radius \(cr\).
All periodic packing \(\mathcal{P} \subseteq \mathbb {R}^8\) has density satisfying \(\Delta _{\mathcal{P}} \leq \Delta _{E_8} = \frac{\pi ^4}{384}\), the density of the \(E_8\) sphere packing (see definition 3.9).
For a periodic sphere packing \(\mathcal{P} = \mathcal{P}(X)\) with centers \(X\) periodic to the lattice \(\Lambda \) and separation \(r\),
Let \(F\) be a holomorphic quasimodular cusp form with real Fourier coefficients. Assume that there exists \(k\) such that \((\partial _{k}F)(it) {\gt} 0\) for all \(t {\gt} 0\). If the first Fourier coefficient of \(F\) is positive, then \(F(it) {\gt} 0\) for all \(t {\gt} 0\).
Let \(X\subset \mathbb {R}^d\) be a discrete subset such that \(\| x-y\| \geq 1\) for any distinct \(x,y\in X\). Suppose that \(X\) is \(\Lambda \)-periodic with respect to some lattice \(\Lambda \subset \mathbb {R}^d\). Let \(f:\mathbb {R}^d\to \mathbb {R}\) be a Schwartz function that is not identically zero and satisfies the following conditions:
and
Then the density of any \(\Lambda \)-periodic sphere packing is bounded above by
There exists a radial Schwartz function \(g:\mathbb {R}^8\to \mathbb {R}\) which satisfies:
For all \(d\), the periodic sphere packing constant in \(\mathbb {R}^d\) is equal to the sphere packing constant in \(\mathbb {R}^d\).
Let \(\Lambda \) be a lattice in \(\mathbb {R}^d\), and let \(f:\mathbb {R}^d\to \mathbb {R}\) be a Schwartz function. Then, for all \(v \in \mathbb {R}^d\),
We have
Serre derivative \(\partial _{k}\) is equivariant with the slash action of \(\mathrm{SL}_{2}(\mathbb {Z})\) in the following sense:
Let \(F\) be a modular form of weight \(k\) and level \(\Gamma \). Then, \(\partial _{k}F\) is a modular form of weight \(k + 2\) of the same level.