Let X_D = X \cap D be the N centers in the fundamental region. Since every center is uniquely y + \lambda with y \in X_D and \lambda \in \Lambda (SpherePacking.CohnElkies.fundamentalCentersLatticeProductEquiv), the double sum of f over X \times X_D can be written as \sum_{x \in X_D}\sum_{y \in X_D}\sum_{\lambda\in\Lambda} f(x - y + \lambda) (SpherePacking.CohnElkies.center_double_sum_eq_region_lattice_sum). For x \ne y, or for x = y and \lambda \ne 0, the point x - y + \lambda is a difference of distinct centers, so it has norm at least 1 and f is nonpositive there; hence each inner lattice sum is at most f(0) if x = y and at most 0 otherwise (SpherePacking.CohnElkies.real_lattice_sum_bounded_by_origin_term), and the double sum is at most N f(0) (packing_bound_auxiliary_estimate).

On the other hand, Poisson summation Theorem 2.2.1 applied to each inner sum with v = x - y, followed by an exchange of the finite sums over x, y with the absolutely convergent spectral sum (SpherePacking.CohnElkies.packing_spectral_sum_exchange), identifies the double sum with \dfrac{1}{\operatorname{covol}(\Lambda)}\sum_{m\in\Lambda^*}\widehat f(m)\,|S(m)|^2, S(m) = \sum_{x\in X_D}e^{2\pi i\langle x,m\rangle}, (packing_bound_geometric_estimate). Every term is nonnegative because \widehat f \ge 0 (SpherePacking.CohnElkies.nonnegative_weighted_nonzero_frequency_sum), and the term m = 0 equals N^2\widehat f(0)/\operatorname{covol}(\Lambda) (packing_bound_spectral_estimate). Combining the two estimates gives N/\operatorname{covol}(\Lambda) \le f(0)/\widehat f(0), and the density formula Lemma 2.1.8 turns this into the claim.