The high-level idea is to prove that \mathcal{P} \cap \mathcal{B}_d(R) = \left(\bigcup_{x \in X} \mathcal{B}_d\left(x, \frac{r}{2}\right)\right) \subseteq \bigcup_{x \in X \cap \mathcal{B}_d\left(R + \frac{r}{2}\right)} \mathcal{B}_d\left(x, \frac{r}{2}\right), and a similar inequality for the lower bound. The rest follows by rearranging and using the fact that the balls are pairwise disjoint in [??].

For the first inequality, it suffices to prove that \mathcal{B}_d(R - L) \subseteq \bigcup_{x \in \Lambda \cap \mathcal{B}_d(R)} (x + \mathcal{D}), since the cosets on the right are disjoint. For a vector v \in \mathcal{B}_d(R - L), we have \|v\| < R - L by definition. Since \mathcal{D} is a fundamental domain, there exists a lattice point x \in \Lambda such that v \in x + \mathcal{D}. Rearranging gives v - x \in \mathcal{D}, which means \|v - x\| \leq L. By the triangle inequality, \|x\| < R, so x \in \mathcal{B}_d(R). /- source paragraph break -/ For the second inequality, we prove that \bigcup_{x \in \Lambda \cap \mathcal{B}_d(R)} (x + \mathcal{D}) \subseteq \mathcal{B}_d(R + L). Consider a vector x \in \Lambda \cap \mathcal{B}_d(R) and a vector y \in x + \mathcal{D}. Then \|x\| < R and \|y - x\| \leq L, so \|y\| < R + L, concluding the proof.

For the first inequality, we notice that \bigcup_{x \in \Lambda \cap \mathcal{B}_d(R - L)} (x + \mathcal{D}) \subseteq \mathcal{B}_d(R), because for x \in \Lambda \cap \mathcal{B}_d(R - L) and y \in x + \mathcal{D}, we have \|x\| < R - L and \|y - x\| \leq L, so \|y\| < R by the triangle inequality. Intersecting both sides with X and simplifying, we get \left(\bigcup_{x \in \Lambda \cap \mathcal{B}_d(R - L)} (x + \mathcal{D})\right) \cap X = \bigcup_{x \in \Lambda \cap \mathcal{B}_d(R - L)} ((x + \mathcal{D}) \cap X) \subseteq \mathcal{B}_d(R) \cap X. Taking cardinalities and noting that |(x + \mathcal{D}) \cap X| = |X / \Lambda| for all x, we obtain |\Lambda \cap \mathcal{B}_d(R - L)||X / \Lambda| \leq |X \cap \mathcal{B}_d(R)|. /- source paragraph break -/ The proof of the second inequality is similar. We again observe that \mathcal{B}_d(R) \subseteq \bigcup_{x \in \Lambda \cap \mathcal{B}_d(R + L)} (x + \mathcal{D}), which follows from the tiling property of a fundamental domain. Intersecting both sides with X and taking cardinalities concludes the proof. /- source paragraph break -/ There are several technicalities when formalising in Lean, such as having to prove that |\Lambda \cap \mathcal{B}_d(R)| is countable and finite. Those are handled in aux3.

Write out the formula for the volume of a ball and simplify. More specifically, we have \mathrm{Vol}(\mathcal{B}_d(R)) = R^d \pi^{d / 2} / \Gamma\left(\frac{d}{2} + 1\right), so \mathrm{Vol}(\mathcal{B}_d(R)) / \mathrm{Vol}(\mathcal{B}_d(R + C)) = R^d / (R + C)^d = \left(1 - \frac{1}{R + C}\right)^d, which tends to 1.

Fix any fundamental domain \mathcal{D} (induced by any basis) of the lattice \Lambda. Combining Lemma 3.1, Lemma 3.2 and Lemma 3.3, we get the following inequality for the finite density: |X / \Lambda| \cdot \frac{\Vol{\mathcal{B}_d(r / 2)}}{\Vol{\R^d / \Lambda}} \cdot \frac{\Vol{\mathcal{B}_d(R - r / 2 - 2L)}}{\Vol{\mathcal{B}_d(R)}} \leq \Delta_{\mathcal{P}}(R) \leq |X / \Lambda| \cdot \frac{\Vol{\mathcal{B}_d(r / 2)}}{\Vol{\R^d / \Lambda}} \cdot \frac{\Vol{\mathcal{B}_d(R + r / 2 + 2L)}}{\Vol{\mathcal{B}_d(R)}}. Taking limit on both sides as R \to \infty and apply the Sandwich theorem and Lemma 3.4, we get \Delta_{\mathcal{P}} = \limsup_{R \to \infty} \Delta_{\mathcal{P}}(R) = \lim_{R \to \infty} \Delta_{\mathcal{P}}(R) = |X / \Lambda| \cdot \frac{\Vol{\mathcal{B}_d(r / 2)}}{\Vol{\R^d / \Lambda}}.