1 Introduction

The long-standing twin prime conjecture asserts that, if $p_{n}$ is the $n$ -th prime, then $n \to \infty lim inf (p_{n + 1} - p_{n}) = 2.$ One of many reasons for the difficulty of the conjecture is the fact that it imposes additive structure on primes, which are defined multiplicatively. The twin prime conjecture is a special case of a more general conjecture, the Hardy–Littlewood $k$ -tuples conjecture, which we now state. Suppose that $H_{k} = {h_{1}, \dots, h_{k}}$ is an admissible set (Definition 3.15). The conjecture then states that there are infinitely many positive integers $n$ such that each of the numbers $n + h_{1}, \dots, n + h_{k}$ is prime. Since ${0, 2}$ is an admissible set, the Hardy–Littlewood $k$ -tuples conjecture implies the twin prime conjecture.

The prime number theorem implies that as $n \to \infty$ , the average value of $p_{n + 1} - p_{n}$ is asymptotic to $lo g p_{n}$ . Foundational work of Goldston, Pintz, and Yıldırım developed the “GPY method,” which led to the proof that $n \to \infty lim inf \frac{p _{n + 1} - p _{n}}{lo g p _{n}} = 0.$ Their method crucially relies on the distribution of primes in arithmetic progressions given by the Bombieri–Vinogradov theorem: If $0 < ε < \frac{1}{2}$ and $A > 0$ are fixed, then for all $x \geq 2$ , $q \leq x^{1/2 - ε} \sum g c d (a, q) = 1 max π (x; q, a) - \frac{π ( x )}{φ ( q )} ≪_{A} \frac{x}{( lo g x ) ^{A}} .$ The Elliott–Halberstam conjecture asserts that $x^{1/2 - ε}$ can be replaced with $x^{1 - ε}$ . If there exists a fixed $δ > 0$ such that $1/2 - ε$ can be improved to $1/2 + δ$ , then the GPY method suffices to establish the infinitude of bounded gaps between primes, namely $n \to \infty lim inf (p_{n + 1} - p_{n}) < \infty.$

In May 2013, Zhang established deep new results on the distribution of primes in arithmetic progressions, a variant of the Bombieri–Vinogradov theorem. When combined with a modification of the GPY method, it yields for the first time the existence of infinitely many bounded gaps between primes: $n \to \infty lim inf (p_{n + 1} - p_{n}) \leq 70000 000.$ The work of Zhang was meticulously refined by the Polymath 8a project, the net result of which was the bound $n \to \infty lim inf (p_{n + 1} - p_{n}) \leq 4 680.$

In November 2013, the breakthrough work of Maynard¹ established a substantially more robust version of the GPY method that leads to significant theoretical and numerical improvements over the work of Zhang using only the original Bombieri–Vinogradov theorem. Writing $H_{m} := n \to \infty lim inf (p_{m + n} - p_{n}),$ Maynard proved that $H_{m} ≪ m^{3} e^{4 m}$ , and in particular that $H_{1} \leq 600$ . Shortly thereafter, the Polymath8b project theoretically and numerically refined these ideas, obtaining $H_{m} ≪ m e^{(4 - \frac{28}{157}) m}$ and in particular $H_{1} \leq 246$ .

This blueprint develops the bound $H_{1} \leq 246$ from a multidimensional sieve. The only result that is assumed is the Bombieri–Vinogradov theorem.

Theorem (Main result). Assume the Bombieri–Vinogradov theorem. Then $H_{1} \leq 246$ ; that is, $n \to \infty lim inf (p_{n + 1} - p_{n}) \leq 246.$

2 Overview

We give a blueprint of the proof of the bound of Section 1, in a form meant to be formalized in Lean. This section outlines the method; the rest of the paper carries it out. Throughout, the only analytic input is the Bombieri–Vinogradov theorem.

2.1 The GPY method and the sum $S_{2} (λ) - ρ S_{1} (λ)$

Fix an admissible $k$ -tuple $H = {h_{1}, \dots, h_{k}}$ (Definition 3.15); we seek infinitely many $n$ for which at least $⌊ ρ ⌋ + 1$ of $n + h_{1}, \dots, n + h_{k}$ are prime. Following Goldston–Pintz–Yıldırım, introduce weights $w_{n} \geq 0$ and set $S (N, ρ) := N < n \leq 2 N \sum (i = 1 \sum k χ_{P} (n + h_{i}) - ρ) w_{n},$ with $χ_{P}$ the characteristic function of the primes. If $S (N, ρ) > 0$ for all large $N$ , then infinitely many $n$ have at least $⌊ ρ ⌋ + 1$ of the $n + h_{i}$ prime: some summand is positive, and since $w_{n} \geq 0$ that $n$ satisfies $\sum_{i} χ_{P} (n + h_{i}) > ρ$ . Writing $S_{1} (λ) S_{2} (λ) = = N < n \leq 2 N \sum w_{n}, N < n \leq 2 N \sum (i \sum χ_{P} (n + h_{i})) w_{n},$ we have $S (N, ρ) = S_{2} (λ) - ρ S_{1} (λ) .$ One chooses $w_{n}$ to make $S_{2} (λ) / S_{1} (λ)$ large.

2.2 The sieve weights and the $W$ -trick

Maynard’s weights are $w_{n} = (d_{i} ∣ n + h_{i} \forall i \sum λ (d_{1}, \dots, d_{k}))^{2}, λ : N^{k} \to R,$ supported on $\prod_{i} d_{i} \leq R$ , where $R$ is a truncation parameter below the level of distribution $ϑ$ . The one-dimensional choice $λ (d_{1}, \dots, d_{k}) = μ (d) F (lo g (R / d))$ with $d = d_{1} \dots d_{k}$ recovers the Selberg weights of Goldston–Pintz–Yıldırım; for these the level $ϑ < 1/2$ does not suffice to make $S_{2} (λ) - ρ S_{1} (λ) > 0$ for any $ρ \geq 1$ , and it is the extra freedom of the $k$ -dimensional $λ$ that removes this obstruction. The $λ (d_{1}, \dots, d_{k})$ are built from a fixed profile $F$ on a subset of $R^{k}$ fixed in Section 5.

To handle small primes, we restrict $w_{n}$ to be nonzero only for $n$ in a single residue class $v_{0} (mod W)$ , where $W = \prod_{p \leq D_{0}} p$ and $D_{0} = lo g lo g lo g N$ . By admissibility of $H$ and the Chinese remainder theorem there is a $v_{0}$ with $v_{0} + h_{i}$ coprime to $W$ for every $i$ , so no prime $p \leq D_{0}$ divides any $n + h_{i}$ .

2.3 The variational problem

Write $R_{k} (s) := {t \in R_{\geq 0}^{k} : t_{1} + \dots + t_{k} \leq s}$ for the standard simplex scaled to total mass $s$ , and $R_{k} := R_{k} (1)$ . Fix $ε \geq 0$ and take $F$ supported on $R_{k} (1 + ε)$ . With $W$ the primorial of the $W$ -trick, the sieve sums satisfy $S_{1} (λ) S_{2} (λ) = (1 + o (1)) \frac{φ ( W ) ^{k}}{W ^{k + 1}} N (lo g R)^{k} I_{k} (F), = (1 + o (1)) \frac{lo g R}{lo g N} \frac{φ ( W ) ^{k}}{W ^{k + 1}} N (lo g R)^{k} m = 1 \sum k J_{k, ε}^{(m)} (F),$ where $I_{k} (F) = \int_{R_{k} (1 + ε)} F^{2}$ and $J_{k, ε}^{(m)} (F)$ is the $L^{2}$ mass of the $m$ th marginal $\int F d t_{m}$ over the slice $R_{k - 1} (1 - ε)$ (Section 5 gives the precise definitions). Since $lo g R = (ϑ /2 - δ) lo g N$ , $\frac{S _{2} ( λ )}{S _{1} ( λ )} M_{k, ε} \sim := (\frac{ϑ}{2} - δ) M_{k, ε}, F sup \frac{\sum _{m = 1}^{k} J _{k, ε}^{(m)} ( F )}{I _{k} ( F )} .$ Provided $ϑ$ and $ε$ satisfy a compatibility condition, $S (N, ρ)$ is eventually positive when $ρ < (ϑ /2) M_{k, ε}$ ; two of the $n + h_{i}$ are then prime for infinitely many $n$ , giving a gap at most the diameter of $H$ , once $M_{k, ε} > 2/ ϑ$ .

The bound $H_{1} \leq 246$ is the case $ε = 1/25$ , $k = 50$ . Enlarging the support to $R_{k} (1 + ε)$ raises the supremum to $M_{50, 1/25} > 4.0043$ , exhibited by an explicit $F$ from a finite basis of symmetric polynomials, for which the ratio is a quotient of rational quadratic forms verified by the certificate of Section 12. With an admissible $50$ -tuple of diameter $246$ this gives $H_{1} \leq 246$ .

Bombieri–Vinogradov supplies every $ϑ < 1/2$ . The remaining input is the finite numerical inequality $M_{50, 1/25} > 4.0043$ , which we prove by exact computation.

3 Definitions and preliminaries

This section collects the objects and standard facts used throughout: the classical arithmetic functions, admissible sets, the level of distribution and the two external inputs (Bombieri–Vinogradov and the prime number theorem), the $W$ -trick, and the truncation parameter $R$ with the support condition it imposes on the sieve weights.

3.1 Arithmetic functions and standard notation

Notation 3.1 (Standard symbols). We write $N = {1, 2, 3, \dots}$ for the positive integers and $P = {2, 3, 5, \dots}$ for the primes. For integers $a, b$ we write $(a, b) = g cd (a, b)$ and $[a, b] = lcm (a, b)$ , and we call $a$ and $b$ coprime when $(a, b) = 1$ . For real $x$ we write $⌊ x ⌋$ and $⌈ x ⌉$ for the floor and the ceiling. Finally, $χ_{P} : N \to {0, 1}$ denotes the indicator function of the primes, so that $χ_{P} (n) = 1$ if $n \in P$ and $χ_{P} (n) = 0$ otherwise.

Lean: PrimeGaps.primeIndicator

Notation 3.2 (Asymptotic notation). For real-valued functions $f, g$ , the statement $f ≪ g$ means $∣ f ∣ \leq C ∣ g ∣$ for some constant $C$ , which may depend on the tuple length $k$ and on $H$ (both fixed throughout) but never on $N$ . A subscript, as in $f ≪_{A} g$ , records an additional permitted dependence of $C$ . We write $f = O (g)$ for $f ≪ g$ , and $f = o (g)$ when $f / g \to 0$ as $N \to \infty$ .

Lean: Asymptotics.IsBigO, Asymptotics.IsLittleO

Definition 3.3 (Möbius function $μ$ ). The Möbius function $μ : N \to {- 1, 0, 1}$ is defined by $μ (n) := ⎩ ⎨ ⎧ 1 (- 1)^{r} 0 if n = 1, if n = p_{1} p_{2} \dots p_{r} is a product of r distinct primes, if p^{2} ∣ n for some prime p .$

Lean: ArithmeticFunction.moebius

Definition 3.4 (Euler totient $φ$ ). The Euler totient function $φ : N \to N$ is defined by $φ (n) := # {a \in {1, 2, \dots, n} : (a, n) = 1} .$

Lean: ArithmeticFunction.totient

Definition 3.5 ( $r$ -fold divisor function $τ_{r}$ ). For an integer $r \geq 0$ , the $r$ -fold divisor function $τ_{r} : N \to N$ counts ordered factorisations into $r$ positive-integer factors: $τ_{r} (n) := # {(d_{1}, d_{2}, \dots, d_{r}) \in N^{r} : d_{1} d_{2} \dots d_{r} = n} .$ We abbreviate $τ := τ_{2}$ , the ordinary divisor-counting function $τ (n) = # {d \geq 1 : d ∣ n}$ .

Lean: ArithmeticFunction.tau_apply_eq_card_finMulAntidiag, ArithmeticFunction.termτ_

Definition 3.6 (The function $g$ ). Let $g : N \to N$ be the multiplicative function determined on prime powers by $g (p) g (p^{a}) := := p - 2, p^{a - 2} (p - 1)^{2} (a \geq 2),$ for every prime $p$ , together with $g (1) = 1$ .

Lean: ArithmeticFunction.detotient

Lemma 3.7 (Möbius divisor-sum identity). For every positive integer $s$ , $t ∣ s \sum μ (t) = 1 [s = 1] .$

Lean: ArithmeticFunction.sum_divisors_coe_moebius, ArithmeticFunction.sum_divisors_moebius

Uses: Definition 3.3

Proof. If $s = 1$ , the only divisor is $t = 1$ and $μ (1) = 1$ by Definition 3.3, so the sum equals $1$ . Suppose $s > 1$ and let $p_{1}, \dots, p_{r}$ ( $r \geq 1$ ) be the distinct primes dividing $s$ . By Definition 3.3, $μ (t) = 0$ unless $t$ is squarefree, so only the $2^{r}$ divisors of $p_{1} \dots p_{r}$ contribute, and such a divisor $t = \prod_{i \in I} p_{i}$ contributes $(- 1)^{∣ I ∣}$ . Grouping by $∣ I ∣$ gives $t ∣ s \sum μ (t) = j = 0 \sum r (j r) (- 1)^{j} = (1 - 1)^{r} = 0$ by the binomial theorem, since $r \geq 1$ . ◻

Lemma 3.8 (Submultiplicativity of $τ_{r}$ ). For every integer $r \geq 0$ and all positive integers $m, n$ , $τ_{r} (mn) \leq τ_{r} (m) τ_{r} (n),$ with equality when $(m, n) = 1$ .

Lean: ArithmeticFunction.isMultiplicative_tau, ArithmeticFunction.isSubmultiplicative_tau

Uses: Definition 3.5

Proof. By Definition 3.5, $τ_{r}$ is the $r$ -fold Dirichlet convolution of the constant function $1$ with itself. Convolution preserves multiplicativity, whence $τ_{r} (mn) = τ_{r} (m) τ_{r} (n)$ whenever $(m, n) = 1$ ; this gives the asserted equality.

For the inequality in general, it suffices to produce an injection from the ordered $r$ -fold factorisations of $mn$ into the pairs consisting of an ordered $r$ -fold factorisation of $m$ and one of $n$ . Fix a factorisation $mn = d_{1} \dots d_{r}$ . For each prime $p$ distribute the exponent $v_{p} (d_{i})$ between $m$ and $n$ by the greedy rule: assign to the $m$ -part the first $min (v_{p} (d_{i}), remaining exponent of p in m)$ of the copies of $p$ occurring in $d_{i}$ , processing $i = 1, \dots, r$ in order, and assign the rest to the $n$ -part. This produces factorisations $m = a_{1} \dots a_{r}$ and $n = b_{1} \dots b_{r}$ with $d_{i} = a_{i} b_{i}$ , and the original factorisation is recovered from the pair, so the assignment is injective. Hence $τ_{r} (mn) \leq τ_{r} (m) τ_{r} (n)$ . ◻

Lemma 3.9 (Equality $τ_{r} (n)^{2} = τ_{r^{2}} (n)$ on squarefree integers). For every integer $r \geq 0$ and every squarefree positive integer $n$ , $τ_{r} (n)^{2} = τ_{r^{2}} (n) .$

Lean: ArithmeticFunction.tau_sq_eq_tau_sq

Uses: Definition 3.5

Proof. Both sides are multiplicative in $n$ by Lemma 3.8, so for squarefree $n = p_{1} \dots p_{s}$ with distinct primes $p_{i}$ it suffices to verify the identity at a single prime argument. An ordered $r$ -fold factorisation of a prime $p$ has exactly one factor equal to $p$ and all others equal to $1$ , so $τ_{r} (p) = r$ ; likewise $τ_{r^{2}} (p) = r^{2}$ . Hence $τ_{r} (p)^{2} = r^{2} = τ_{r^{2}} (p)$ , and multiplying over $p_{1}, \dots, p_{s}$ gives $τ_{r} (n)^{2} = τ_{r^{2}} (n)$ . (The hypothesis that $n$ be squarefree is essential: for $n = p^{2}$ one has $τ_{r} (p^{2})^{2} = (2 r + 1)^{2} < (2 r ^{2} + 1) = τ_{r^{2}} (p^{2})$ in general.) ◻

Proof uses: Lemma 3.8

Lemma 3.10 (Dirichlet convolution identity $φ = g * 1$ ). For every positive integer $n$ , $φ (n) = u ∣ n \sum g (u) .$

Lean: Nat.totient_eq_sum_divisors_g

Uses: Definition 3.6, Definition 3.4

Proof. Both sides are multiplicative functions of $n$ : this is standard for $φ$ , and the divisor sum of the multiplicative function $g$ (Definition 3.6) is again multiplicative. It therefore suffices to compare the two sides at a prime power $n = p^{a}$ with $a \geq 1$ .

For $a = 1$ , $u ∣ p \sum g (u) = g (1) + g (p) = 1 + (p - 2) = p - 1 = φ (p) .$ For $a \geq 2$ , using $g (p^{j}) = p^{j - 2} (p - 1)^{2}$ for $2 \leq j \leq a$ , $u ∣ p^{a} \sum g (u) = 1 + (p - 2) + (p - 1)^{2} j = 2 \sum a p^{j - 2} = (p - 1) + (p - 1)^{2} \cdot \frac{p ^{a - 1} - 1}{p - 1} = (p - 1) p^{a - 1},$ which is $φ (p^{a})$ . Multiplicativity now gives the identity for every $n$ . ◻

Lemma 3.11 (Euler product identity for $\sum_{d ∣ n} μ (d) / d$ ). For every positive integer $n$ , $d ∣ n \sum \frac{μ ( d )}{d} = \frac{φ ( n )}{n} = p ∣ n \prod (1 - \frac{1}{p}) .$

Lean: ArithmeticFunction.sum_moebius_div_self, Nat.totient_div_self_eq_prod

Uses: Definition 3.3, Definition 3.4

Proof. The function $n \mapsto \sum_{d ∣ n} μ (d) / d$ is the Dirichlet convolution of the multiplicative function $d \mapsto μ (d) / d$ with the constant function $1$ , hence multiplicative. Evaluating at a prime power $p^{a}$ with $a \geq 1$ and using $μ (p^{j}) = 0$ for $j \geq 2$ (Definition 3.3), $d ∣ p^{a} \sum \frac{μ ( d )}{d} = \frac{μ ( 1 )}{1} + \frac{μ ( p )}{p} = 1 - \frac{1}{p} .$ Hence, writing $n = \prod_{p ∣ n} p^{a_{p}}$ , the divisor sum equals $\prod_{p ∣ n} (1 - 1/ p)$ . On the other hand $φ$ is multiplicative with $φ (p^{a}) = p^{a} (1 - 1/ p)$ (Definition 3.4), so $φ (n) / n = \prod_{p ∣ n} (1 - 1/ p)$ as well. The two displayed equalities follow. ◻

Lemma 3.12 (Dirichlet expansion of $n / φ (n)$ ). For every positive integer $n$ , $\frac{n}{φ ( n )} = e ∣ n \sum \frac{μ ( e ) ^{2}}{φ ( e )} .$

Lean: ArithmeticFunction.sum_moebius_sq_div_totient, ArithmeticFunction.sum_squarefree_totient_inv, ArithmeticFunction.sum_totient_inv

Uses: Definition 3.3, Definition 3.4

Proof. Both sides are multiplicative in $n$ ; for the right-hand side this is because $μ^{2}$ and $1/ φ$ are multiplicative and the divisor sum of a multiplicative function is multiplicative. It therefore suffices to compare at a prime power $n = p^{a}$ with $a \geq 1$ . Since $μ (p^{j})^{2} = 0$ for $j \geq 2$ , $e ∣ p^{a} \sum \frac{μ ( e ) ^{2}}{φ ( e )} = \frac{1}{φ ( 1 )} + \frac{1}{φ ( p )} = 1 + \frac{1}{p - 1} = \frac{p}{p - 1} = \frac{p ^{a}}{φ ( p ^{a} )},$ the last equality because $φ (p^{a}) = p^{a - 1} (p - 1)$ . Multiplicativity gives the identity in general. ◻

Lemma 3.13 (Lower bound for $φ$ in terms of $τ$ ). For every positive integer $n$ , $n \frac{n}{τ ( n )} \leq \leq τ (n) φ (n), equivalently φ (n) .$

Lean: ArithmeticFunction.div_tau₂_le_totient, ArithmeticFunction.le_tau₂_mul_totient, Nat.inv_d_totient_le

Uses: Definition 3.4, Definition 3.5

Proof. Write $n = \prod_{i = 1}^{r} p_{i}^{a_{i}}$ with distinct primes $p_{i}$ , so $r = ω (n)$ and $τ (n) = \prod_{i} (a_{i} + 1) \geq 2^{r}$ . For every prime $p \geq 2$ we have $1 - 1/ p \geq 1/2$ , hence by Lemma 3.11 $\frac{φ ( n )}{n} = i = 1 \prod r (1 - \frac{1}{p _{i}}) \geq 2^{- r} \geq \frac{1}{τ ( n )} .$ Multiplying through by $n τ (n)$ gives $n \leq τ (n) φ (n)$ . ◻

Proof uses: Lemma 3.11

Lemma 3.14 (Union bound for finite sums). Let $X$ be a finite index set, let ${A_{x}}_{x \in X}$ be finite subsets of an ambient set, and write $1_{A}$ for the indicator function of $A$ . Then, for every point $y$ , $1_{⋃_{x \in X} A_{x}} (y) \leq x \in X \sum 1_{A_{x}} (y) .$

Proof. If $y \in / ⋃_{x} A_{x}$ both sides are $0$ . If $y \in ⋃_{x} A_{x}$ , then $y \in A_{x_{0}}$ for at least one $x_{0} \in X$ , so the left-hand side equals $1$ while the right-hand side is a sum of non-negative terms one of which equals $1$ ; the inequality follows. ◻

Throughout the blueprint, Lemma 3.14 is applied in the following form. Given a sum $Σ = \sum_{t \in T} c (t)$ of non-negative terms and a covering $T = ⋃_{x \in X} T_{x}$ by finitely many sub-events, multiplying the displayed indicator inequality by $c (t) \geq 0$ and summing yields $Σ \leq x \in X \sum t \in T_{x} \sum c (t) .$ The phrase “apply the union bound over the choices of $x$ ” denotes this passage.

3.2 Admissible sets

Definition 3.15 (Admissible set). Let $k \in N$ . A finite set $H = {h_{1}, \dots, h_{k}} \subset Z_{\geq 0}$ of $k$ distinct non-negative integers is admissible if, for every prime $p$ , there exists an integer $a_{p}$ with $a_{p} \neq \equiv h_{i} (mod p) for every i \in {1, \dots, k} .$

Lean: Finset.Admissible

Lemma 3.16 (Cardinality characterisation of admissibility). A finite set $H \subset Z_{\geq 0}$ is admissible (Definition 3.15) if and only if $# {h mod p : h \in H} < p for every prime p .$

Lean: PrimeGaps.lem_admissible_cardinality_char

Uses: Definition 3.15

Proof. Fix a prime $p$ and set $S_{p} := {h mod p : h \in H} \subseteq Z / p Z$ . There exists $a_{p}$ with $a_{p} \neq \equiv h_{i} (mod p)$ for every $i$ if and only if $S_{p} \neq = Z / p Z$ : given such an $a_{p}$ , its residue class is missing from $S_{p}$ ; conversely, if $S_{p} ⊊ Z / p Z$ , any representative of a class not in $S_{p}$ will do. Since $Z / p Z$ is finite of cardinality $p$ , the condition $S_{p} \neq = Z / p Z$ is equivalent to $# S_{p} < p$ . Applying this for every prime $p$ gives the claim. ◻

Lemma 3.17 (Admissibility is a finite check). A finite set $H \subset Z_{\geq 0}$ is admissible (Definition 3.15) if and only if, for every prime $p \leq # H$ , there exists $a < p$ with $h \neq \equiv a (mod p)$ for every $h \in H$ .

Lean: Finset.admissible_iff_le_card

Uses: Definition 3.15

Proof. Admissibility trivially implies the stated condition, since the latter only restricts the primes $p \leq # H$ and, as in the proof of Lemma 3.16, one may always replace a missed residue by its representative in ${0, 1, \dots, p - 1}$ .

Conversely, assume the condition and let $p$ be an arbitrary prime. If $p \leq # H$ there is nothing to prove. If $p > # H$ , then the image of $H$ in $Z / p Z$ has at most $# H < p$ elements, so it is a proper subset of $Z / p Z$ and some residue class is missed; by Lemma 3.16 this is exactly what admissibility requires at $p$ . Hence $H$ is admissible. ◻

Proof uses: Lemma 3.16

Lemma 3.17 reduces admissibility — a condition on all primes — to a finite verification, so the admissibility of an explicit tuple is decidable.

Definition 3.18 (Diameter of $H$ ). Let $H = {h_{1}, \dots, h_{k}}$ be a finite non-empty set of non-negative integers. The diameter of $H$ is $diam (H) := 1 \leq i, j \leq k max (h_{i} - h_{j}) .$

Lean: Finset.diameter

Lemma 3.19 (Diameter as largest minus smallest). Let $H = {h_{1}, \dots, h_{k}}$ be a finite non-empty set of non-negative integers, labelled so that $h_{1} < h_{2} < \dots < h_{k}$ . Then $diam (H) = h_{k} - h_{1} .$

Lean: Finset.diameter_eq_max_sub_min

Uses: Definition 3.18

Proof. The pair $(i, j) = (k, 1)$ is admissible in the maximum of Definition 3.18 and contributes $h_{k} - h_{1}$ , so $diam (H) \geq h_{k} - h_{1}$ . Conversely, for any $i, j$ we have $h_{i} \leq h_{k}$ and $h_{j} \geq h_{1}$ , whence $h_{i} - h_{j} \leq h_{k} - h_{1}$ ; taking the maximum over $i, j$ gives $diam (H) \leq h_{k} - h_{1}$ . ◻

3.3 Prime counting and the level of distribution

Notation 3.20 (Prime-counting functions). For real $x$ , a modulus $q \in N$ , a residue $a$ modulo $q$ , and a subset $S \subseteq N$ , set $π_{S} (x) π_{S} (x; q, a) := := # {p \leq x : p \in P, p \in S}, # {p \leq x : p \in P, p \in S, p \equiv a (mod q)} .$ When $S = N$ we drop it from the notation and write $π (x)$ and $π (x; q, a)$ ; these are the classical prime-counting function and its analogue in an arithmetic progression. A real argument is always interpreted through its floor, so $π_{S} (x) = π_{S} (⌊ x ⌋)$ .

Definition 3.21 (Level of distribution). Let $S \subseteq N$ , let $ϑ \in R$ , and let $Ξ \in N$ be an auxiliary modulus. We say that $S$ has level of distribution $ϑ$ relative to $Ξ$ if for every $A \geq 1$ there is a constant $c = c (A) > 0$ such that, for every real $x \geq 3$ , $1 \leq q \leq x^{ϑ} (q, Ξ) = 1 \sum a mod q (a, q) = 1 max π_{S} (x; q, a) - \frac{π _{S} ( x )}{φ ( q )} \leq \frac{c x}{( lo g x ) ^{A}} .$ The unadorned phrase “the primes have level of distribution $ϑ$ ” means that $P$ has level of distribution $ϑ$ relative to $Ξ = 1$ .

Lean: Nat.HasLevelOfDistribution

Uses: Definition 3.4, Notation 3.20

By Definition 3.21, the level of distribution depends on $S$ only through its primes, so the hypothesis may be stated for a set $S$ that is not itself a set of primes.

Lemma 3.22 (Insensitivity to intersecting with the primes). Let $S \subseteq N$ , let $ϑ \in R$ and let $Ξ \in N$ . Then $S \cap P$ has level of distribution $ϑ$ relative to $Ξ$ if and only if $S$ does.

Uses: Definition 3.21

Proof. By Notation 3.20, both $π_{S}$ and $π_{S} (\cdot; q, a)$ count only elements of $S$ that are prime, so $π_{S \cap P} (x) π_{S \cap P} (x; q, a) = = π_{S} (x) and π_{S} (x; q, a)$ for all $x, q, a$ . The two instances of the inequality in Definition 3.21 are therefore literally the same, so each implies the other. ◻

Proof uses: Notation 3.20

Theorem 1 (Bombieri–Vinogradov). For every $θ < 1/2$ , the set $N$ has level of distribution $θ$ relative to $Ξ = 1$ .

Lean: hasLevelOfDistribution_Prime

Uses: Definition 3.21

Proof. This is the classical theorem of Bombieri and Vinogradov, taken as an external input; see Bombieri (1965), Vinogradov (1965), and the textbook treatment in Davenport’s Multiplicative Number Theory. No proof is given here. ◻

Lemma 3.23 (Bombieri–Vinogradov for the primes). Assume Bombieri–Vinogradov (Theorem 1). Then for every $θ < 1/2$ the set $P$ of primes has level of distribution $θ$ relative to $Ξ = 1$ .

Uses: Theorem 1, Definition 3.21

Proof. Fix $θ < 1/2$ . By Theorem 1 the set $N$ has level of distribution $θ$ relative to $1$ . Since $P = N \cap P$ , Lemma 3.22 applied with $S = N$ transfers the property from $N$ to $P$ . ◻

Proof uses: Lemma 3.22

3.4 External analytic inputs

Two analytic results are quoted from the literature: Bombieri–Vinogradov (Theorem 1, above) and the prime number theorem, stated below. Bombieri–Vinogradov is a hypothesis of both main theorems and is never discharged. The prime number theorem is used once, to count the primes in the dyadic interval, and is quoted with a secondary term. The size bound for the primorial $W$ uses Chebyshev-type bounds.

In a proof, “external input” means that the assertion is quoted from the literature and no proof is given here.

Theorem 2 (Prime number theorem with secondary term). There exist a constant $C > 0$ and an integer $N_{0}$ such that, for every integer $N \geq N_{0}$ , $π (N) - \frac{N}{lo g N} \leq \frac{C N}{( lo g N ) ^{2}} .$

Uses: Notation 3.20

Proof. This is the prime number theorem in the form $π (x) = x / lo g x + O (x / (lo g x)^{2})$ , equivalently $ψ (x) = x + O (x / lo g x)$ after partial summation and the passage from $ψ$ to $θ$ to $π$ . It is taken as an external input; no proof is given here. ◻

3.5 Prime counts in a dyadic interval

The sieve runs over the dyadic interval $N < n \leq 2 N$ . The two quantities below count the primes in this window and record their discrepancy in arithmetic progressions.

Notation 3.24 (Prime-counting in $(N, 2 N]$ ). $X_{N} := N < n \leq 2 N \sum χ_{P} (n) = # {p \in P : N < p \leq 2 N} .$

Lean: Nat.primeCountingIoc

Uses: Notation 3.1

Lemma 3.25 ( $X_{N}$ as a difference of prime-counting functions). For every $N \geq 0$ , $X_{N} = π (2 N) - π (N) .$

Lean: PrimeGaps.primeCountingIoc_eq_primeCounting_diff

Uses: Notation 3.24, Notation 3.20

Proof. By Notation 3.20, $π (x) = \sum_{n \leq x} χ_{P} (n)$ , the primes $\leq x$ being counted once each by the indicator $χ_{P}$ . The set of primes $\leq N$ is contained in the set of primes $\leq 2 N$ , so the two counts differ by exactly the primes in $(N, 2 N]$ : $π (2 N) - π (N) = n \leq 2 N \sum χ_{P} (n) - n \leq N \sum χ_{P} (n) = N < n \leq 2 N \sum χ_{P} (n) = X_{N},$ the last equality being Notation 3.24. ◻

Theorem 3 (Prime number theorem for $(N, 2 N]$ ). There exist a constant $C > 0$ and an integer $N_{0}$ such that, for every integer $N \geq N_{0}$ , $X_{N} - \frac{N}{lo g N} \leq \frac{C N}{( lo g N ) ^{2}} .$

Lean: PNT.primeCountingIoc_self_two_mul

Uses: Notation 3.24

Proof. By Lemma 3.25, $X_{N} = π (2 N) - π (N)$ . Let $C_{0}$ and $N_{0}^{'}$ be as furnished by Theorem 2, and take $N \geq max (N_{0}^{'}, 2)$ . Applying Theorem 2 at $2 N$ and at $N$ , and using $lo g (2 N) \geq lo g N$ to weaken the error term at $2 N$ , $π (2 N) - \frac{2 N}{lo g ( 2 N )} π (N) - \frac{N}{lo g N} \leq \leq \frac{2 C _{0} N}{( lo g N ) ^{2}}, \frac{C _{0} N}{( lo g N ) ^{2}} .$ It remains to compare the main terms. Since $lo g (2 N) = lo g 2 + lo g N$ , $\frac{2 N}{lo g ( 2 N )} - \frac{2 N}{lo g N} = - \frac{2 N lo g 2}{( lo g 2 + lo g N ) lo g N},$ whose absolute value is at most $2 N lo g 2/ (lo g N)^{2}$ because $(lo g 2 + lo g N) lo g N \geq (lo g N)^{2}$ . Combining, and writing $X_{N} - \frac{N}{lo g N} = (π (2 N) - \frac{2 N}{lo g 2 N}) - (π (N) - \frac{N}{lo g N}) + (\frac{2 N}{lo g 2 N} - \frac{2 N}{lo g N}),$ the triangle inequality gives the claim with $C = 3 C_{0} + 2 lo g 2$ . ◻

Proof uses: Lemma 3.25, Theorem 2

Notation 3.26 (Local error $E (N, q)$ ). For $q \in N$ , $E (N, q) := 1 + (a, q) = 1 sup N < n \leq 2 N n \equiv a (mod q) \sum χ_{P} (n) - \frac{1}{φ ( q )} N < n \leq 2 N \sum χ_{P} (n),$ the supremum being over the residue classes $a$ modulo $q$ that are coprime to $q$ . The additive $1$ is a convenience: it makes $E (N, q) \geq 1$ , so that $E (N, q)$ may be used as a multiplicative majorant without a separate case for a vanishing discrepancy.

Lean: Nat.primeCountingIocError

Uses: Definition 3.4, Notation 3.24

Lemma 3.27. Assume Bombieri–Vinogradov (Theorem 1). Let $A > 0$ and $ε \in (0, 1/2)$ be fixed. Then there is a constant $C = C (A, ε) > 0$ such that, for every $N \geq 1$ , $1 \leq q \leq N q < N^{1/2 - ε} \sum μ (q)^{2} E (N, q) \leq \frac{C N}{( lo g N ) ^{A}} .$

Lean: PrimeGaps.lem_BV_restated

Uses: Theorem 1, Notation 3.26, Definition 3.3

Proof. Write $Q := {q : 1 \leq q \leq N, q < N^{1/2 - ε}}$ for the range of moduli, and put $θ := 1/2 - ε$ , so that $0 < θ < 1/2$ and $Q \subseteq {q : 1 \leq q \leq N^{θ}}$ .

Step 1: bound $E (N, q)$ by two cumulative discrepancies. Fix $q$ and a residue $a$ coprime to $q$ . The window count $\sum_{N < n \leq 2 N, n \equiv a} χ_{P} (n)$ equals $π (2 N; q, a) - π (N; q, a)$ , and $\sum_{N < n \leq 2 N} χ_{P} (n) = X_{N} = π (2 N) - π (N)$ by Lemma 3.25. Hence the quantity inside the supremum in Notation 3.26 equals $(π (2 N; q, a) - \frac{π ( 2 N )}{φ ( q )}) - (π (N; q, a) - \frac{π ( N )}{φ ( q )}),$ so by the triangle inequality $E (N, q) D (x, q) \leq := 1 + D (2 N, q) + D (N, q), (a, q) = 1 max π (x; q, a) - \frac{π ( x )}{φ ( q )} .$

Step 2: sum over $q \in Q$ . Since $μ (q)^{2} \leq 1$ , summing Step 1 over $q \in Q$ gives $q \in Q \sum μ (q)^{2} E (N, q) \leq # Q + q \in Q \sum D (2 N, q) + q \in Q \sum D (N, q),$ and $# Q \leq N^{1/2 - ε}$ by the definition of $Q$ .

Step 3: apply the level-of-distribution bound. Set $A^{'} := max (A, 1)$ . Since $θ < 1/2$ , Lemma 3.23 says the primes have level of distribution $θ$ relative to $Ξ = 1$ , so Definition 3.21 supplies $c = c (A^{'}) > 0$ with $\sum_{q \leq x^{θ}} D (x, q) \leq c x (lo g x)^{- A^{'}}$ for all $x \geq 3$ . All summands $D (x, q)$ are non-negative, so restricting to $q \in Q \subseteq {q \leq x^{θ}}$ (valid at $x = N$ by the choice of $θ$ , and at $x = 2 N$ since $N^{θ} \leq (2 N)^{θ}$ for $θ \geq 0$ ) yields, for $N \geq 3$ , $q \in Q \sum D (N, q) q \in Q \sum D (2 N, q) \leq \leq \frac{c N}{( lo g N ) ^{A^{'}}} and \frac{2 c N}{( lo g 2 N ) ^{A^{'}}} \leq \frac{2 c N}{( lo g N ) ^{A^{'}}} .$ Moreover $lo g N \geq 1$ for $N \geq 3$ , so $(lo g N)^{- A^{'}} \leq (lo g N)^{- A}$ .

Step 4: absorb the trivial term and the small $N$ . The term $# Q \leq N^{1/2 - ε}$ satisfies $N^{1/2 - ε} \leq K N (lo g N)^{- A}$ for a constant $K = K (A, ε)$ and all $N \geq 2$ : indeed $(lo g N)^{A} ≪_{A, ε} N^{1/2 + ε}$ , and $N^{1/2 - ε} \cdot N^{1/2 + ε} = N$ . Combining Steps 2–4 gives the asserted bound with a suitable constant for all $N$ beyond an explicit threshold; enlarging the constant to accommodate the finitely many remaining $N \geq 1$ (for which the left-hand side is a finite sum, and is empty when $N = 1$ ) gives the lemma. ◻

Proof uses: Lemma 3.25, Lemma 3.23, Definition 3.21, Notation 3.24

3.6 The $W$ -trick

The primes are not equidistributed among the residue classes of a small modulus, and a sieve over $N < n \leq 2 N$ inherits this defect in every local factor. The $W$ -trick removes the obstruction by restricting $n$ to a single residue class $v_{0}$ modulo the product $W$ of all small primes, chosen so that each shifted value $n + h_{i}$ is coprime to $W$ . The cutoff defining “small” is a triple logarithm, large enough for the local factors to converge and small enough that $W$ is negligible against any power of $N$ .

Definition 3.28 (The primorial cutoff $D_{0}$ ). For real $N$ , set $D_{0} := lo g lo g lo g N .$

Lean: PrimeGaps.D₀

Definition 3.29 (The primorial $W$ ). Let $D_{0}$ be as in Definition 3.28. Set $W := p \leq ⌊ D_{0} ⌋ p \in P \prod p,$ the product of all primes not exceeding $⌊ D_{0} ⌋$ (an empty product, equal to $1$ , when $D_{0} < 2$ ).

Lean: Finset.CompatibleWith, PrimeGaps.sieveModulus

Uses: Definition 3.28

Lemma 3.30 (Prime divisors of $W$ ). For every prime $p$ , $p ∣ W ⟺ p \leq D_{0} .$

Uses: Definition 3.29, Definition 3.28

Proof. By Definition 3.29, $W$ is a product of distinct primes, so a prime $p$ divides $W$ if and only if $p$ is one of the factors, that is, if and only if $p \leq ⌊ D_{0} ⌋$ . Since $p$ is an integer, $p \leq ⌊ D_{0} ⌋$ is equivalent to $p \leq D_{0}$ . ◻

Lemma 3.31 ( $W$ is squarefree). $W$ is squarefree.

Uses: Definition 3.29

Proof. By Definition 3.29, $W$ is a product of distinct primes, each occurring to the first power. Hence no prime square divides $W$ , i.e. $W$ is squarefree. ◻

Lemma 3.32 (Size of $W$ ). For all sufficiently large $N$ , $W \leq (lo g lo g N)^{2} .$

Lean: PrimeGaps.lem_W_size

Uses: Definition 3.29, Definition 3.28

Proof. We use the elementary Chebyshev-type bound $\prod_{p \leq n} p \leq 4^{n}$ , valid for every integer $n \geq 0$ ; it is proved by induction on $n$ using the divisibility of $(m 2 m + 1)$ by all primes in $(m + 1, 2 m + 1]$ together with $(m 2 m + 1) \leq 4^{m}$ . No appeal to the prime number theorem is required.

By Definition 3.29 and this bound, $W = p \leq ⌊ D_{0} ⌋ \prod p \leq 4^{⌊ D_{0} ⌋} \leq 4^{D_{0}}$ whenever $D_{0} \geq 0$ . Now $D_{0} = lo g lo g lo g N$ by Definition 3.28, so $e^{D_{0}} = lo g lo g N$ and hence $4^{D_{0}} = e^{D_{0} l o g 4} = (e^{D_{0}})^{l o g 4} = (lo g lo g N)^{l o g 4} .$ Finally $lo g 4 \leq 2$ , so once $N$ is large enough that $lo g lo g N \geq 1$ — equivalently $N \geq e^{e}$ , which also forces $D_{0} \geq 0$ — we may raise the exponent from $lo g 4$ to $2$ and conclude $W \leq (lo g lo g N)^{2}$ . ◻

Definition 3.33 (Compatible residue class $v_{0}$ ). Let $H = {h_{1}, \dots, h_{k}}$ be a finite set of non-negative integers and let $W$ be as in Definition 3.29. An integer $v_{0}$ is compatible with $H$ modulo $W$ if $(v_{0} + h_{i}, W) = 1 for every i \in {1, \dots, k} .$

Uses: Definition 3.29

Lemma 3.34 (Existence of $v_{0}$ ). Let $H$ be an admissible set (Definition 3.15) and let $N$ be arbitrary. Then there exists $v_{0}$ with $0 \leq v_{0} < W$ that is compatible with $H$ modulo $W$ (Definition 3.33).

Lean: Finset.Admissible.exists_compatibleWith

Uses: Definition 3.15, Definition 3.29, Definition 3.33

Proof. By Definition 3.29, $W$ is a product of distinct primes $p \leq ⌊ D_{0} ⌋$ . For each such prime $p$ , admissibility of $H$ (Definition 3.15) supplies a residue $a_{p}$ with $a_{p} \neq \equiv h_{i} (mod p)$ for every $i$ ; equivalently, setting $b_{p} := - a_{p}$ , we have $b_{p} + h_{i} \neq \equiv 0 (mod p)$ for every $i$ .

The primes dividing $W$ are pairwise coprime, so by the Chinese remainder theorem there is an integer $v$ with $v \equiv b_{p} (mod p)$ for every prime $p ∣ W$ . Put $v_{0} := v mod W$ , so $0 \leq v_{0} < W$ and $v_{0} \equiv b_{p} (mod p)$ for each such $p$ .

It remains to check compatibility. Fix $i$ . Since $W$ is squarefree (Lemma 3.31), $(v_{0} + h_{i}, W) = 1$ holds if and only if no prime divisor of $W$ divides $v_{0} + h_{i}$ ; and by Lemma 3.30 the prime divisors of $W$ are exactly the primes $p \leq D_{0}$ , which are the primes handled above. For such a $p$ we have $v_{0} + h_{i} \equiv b_{p} + h_{i} \neq \equiv 0 (mod p)$ by the choice of $b_{p}$ . Hence $(v_{0} + h_{i}, W) = 1$ for every $i$ , i.e. $v_{0}$ is compatible with $H$ modulo $W$ . ◻

Proof uses: Lemma 3.30, Lemma 3.31

Notation 3.35 (Standing notation). We fix throughout: an integer $k \geq 2$ ; an admissible set $H = {h_{1}, \dots, h_{k}}$ with $h_{1} < \dots < h_{k}$ ; the parameters $D_{0}$ and $W$ of Definitions 3.28 and 3.29; and a residue $v_{0}$ compatible with $H$ modulo $W$ (Definition 3.33). All constants implicit in $O (\cdot)$ , $≪$ and $o (\cdot)$ may depend on $k$ and on $H$ , but never on $N$ .

Uses: Definition 3.15, Definition 3.28, Definition 3.29, Definition 3.33, Notation 3.2

3.7 The truncation parameter $R$ and the sieve support

Definition 3.36 (The auxiliary parameter $δ$ ). Let $ϑ$ be a level of distribution (Definition 3.21). Throughout the blueprint, $δ$ denotes a fixed real number in the open interval $δ \in (0, ϑ /2),$ which may be chosen arbitrarily small. The proofs treat $δ$ as a fixed positive constant, and the dependence of error terms on $δ$ is suppressed in the asymptotic notation of Notation 3.2.

Uses: Definition 3.21, Notation 3.2

Definition 3.37 (The truncation $R$ ). Let $δ$ be as in Definition 3.36. The sieve truncation parameter is $R := N^{ϑ /2 - δ} .$

Lean: PrimeGaps.sieveTruncation, PrimeGaps.sieveTruncation.termR

Uses: Definition 3.36

Lemma 3.38 ( $R^{2} W$ lies below $N^{1/2}$ ). Let $ϑ$ and $δ$ be as in Definitions 3.21 and 3.36, let $R$ be as in Definition 3.37, and let $η$ be a real number with $η < \frac{1}{2} - (ϑ - 2 δ) .$ Then, for all sufficiently large $N$ , $R^{2} W \leq N^{1/2 - η} .$

Lean: PrimeGaps.sieve_support_le

Uses: Definition 3.37, Definition 3.29, Definition 3.36, Definition 3.21

Proof. Set $γ := \frac{1}{2} - η - (ϑ - 2 δ)$ , which is positive by hypothesis. By Definition 3.37, $R^{2} = N^{ϑ - 2 δ},$ so it suffices to show that $W \leq N^{γ}$ for all large $N$ , since then $R^{2} W \leq N^{ϑ - 2 δ + γ} = N^{1/2 - η}$ .

By Lemma 3.32, $W \leq (lo g lo g N)^{2}$ for all large $N$ , and $lo g lo g N \leq lo g N$ for $N \geq e$ . Hence $W \leq (lo g N)^{2}$ for all large $N$ . Since $(lo g N)^{2} = o (N^{γ})$ for every $γ > 0$ — powers of the logarithm are dominated by every positive power of $N$ — we obtain $W \leq N^{γ}$ for all large $N$ , as required. ◻

Proof uses: Lemma 3.32

The support condition below is imposed on every sieve weight. It makes the divisor sums finite, keeps the moduli below the Bombieri–Vinogradov range through Lemma 3.38, and decouples the sieve from the small primes absorbed into $W$ .

Definition 3.39 (Permissible support at a truncation level). Let $T$ be a positive integer, the truncation level. A function $λ : N^{k} \to R$ has permissible support at level $T$ if $λ (d_{1}, \dots, d_{k}) = 0$ whenever one of the following three conditions fails:

$\prod_{i = 1}^{k} d_{i} \leq T$ ;
$(\prod_{i = 1}^{k} d_{i}, W) = 1$ ;
$\prod_{i = 1}^{k} d_{i}$ is squarefree.

Two levels occur below. The development on the standard simplex takes $T = ⌊ R ⌋$ , and the development on the enlarged simplex takes $T = ⌊ R^{1 + ε} ⌋$ ; the enlargement buys exactly the longer divisors that the larger level admits. Where the level is clear from context we say simply permissible support.

Lean: Finset.mem_permissibleSupport_iff, Finset.permissibleSupport, Finsupp.HasPermissibleSupport

Uses: Definition 3.37, Definition 3.29

Lemma 3.40 (Permissibility passes to divisors). Let $r = (r_{1}, \dots, r_{k})$ satisfy the three conditions (i)–(iii) of Definition 3.39, and let $d = (d_{1}, \dots, d_{k})$ satisfy $d_{i} ∣ r_{i}$ for every $i$ . Then $d$ satisfies (i)–(iii) as well.

Uses: Definition 3.39

Proof. Since $d_{i} ∣ r_{i}$ for every $i$ , we have $\prod_{i} d_{i} ∣ \prod_{i} r_{i}$ . Because $\prod_{i} r_{i}$ is squarefree it is in particular non-zero, so $\prod_{i} d_{i} \leq \prod_{i} r_{i} \leq R$ , giving (i). A divisor of an integer coprime to $W$ is itself coprime to $W$ , giving (ii), and a divisor of a squarefree integer is squarefree, giving (iii). ◻

Notation 3.41 (Singular series). For a density $γ : N \to R$ the associated singular series is $S (γ) := p \in P \prod \frac{1 - 1/ p}{1 - γ ( p ) / p},$ the product being taken over all primes.

Lean: PrimeGaps.singularSeries, PrimeGaps.singularSeries_primorial, PrimeGaps.term𝔖

4 The sieve datum, the sieve weights, and the auxiliary $y$ -variables

4.1 The sieve datum

The sieve estimates below — the Mertens-type partial summations, the evaluation of the local densities, the singular products — depend on the arithmetic function $γ_{g}$ only through a short list of properties: multiplicativity, a uniform gap between $γ (p)$ and $p$ , closeness of $γ (p)$ to $1$ away from a fixed squarefree modulus, and a two-sided Mertens bound on the weighted prime log-sums. We collect this list as a single object, the sieve datum, consisting of the density $γ$ , the modulus $V$ , and the four constants $A_{1}, A_{2}, A_{3}, L$ . Every statement below is proved for an arbitrary sieve datum and applied twice: once to the $W$ -tricked density $γ_{g}$ , and once, through the same lemmas with a different modulus, in the $r_{i}$ -coordinate analysis of $S_{2}^{(m)}$ .

Definition 4.1 (Mertens deviation of a weight). Let $f : N \to R$ and let $2 \leq w \leq z$ be real. The Mertens deviation of $f$ on $[w, z]$ is $Δ (f; w, z) := w \leq p \leq z p \in P \sum \frac{f ( p ) lo g p}{p} - lo g (z / w) .$

Definition 4.2 (Density). A density is a function $γ : N \to R$ such that

$γ (n) \geq 0$ for every $n$ ;
$γ (1) = 1$ ;
$γ (mn) = γ (m) γ (n)$ whenever $(m, n) = 1$ ;
$γ (p) < p$ for every prime $p$ .

Definition 4.3 (Sieve datum). A sieve datum is a tuple $S = (γ, V, A_{1}, A_{2}, A_{3}, L)$ consisting of a function $γ : N \to R$ , an integer $V \geq 1$ , and real numbers $A_{1}, A_{2}, A_{3}, L$ , subject to the following axioms.

Density. $γ$ is a density in the sense of Definition 4.2.
Growth. $0 < A_{1} < 1$ and $γ (p) / p \leq 1 - A_{1}$ for every prime $p$ .
Modulus. $V$ is squarefree, and $γ (p) = 0$ for every prime $p ∣ V$ .
Unit density off the modulus. $A_{3} \geq 0$ and $∣ γ (p) - 1∣ \leq A_{3} / p$ for every prime $p ∤ V$ .
Mertens. $A_{2} > 0$ , $L \geq 0$ , and $- L \leq Δ (γ; w, z) \leq A_{2}$ for all real $2 \leq w \leq z$ , with $Δ$ as in Definition 4.1.

We call $γ$ the density, $V$ the modulus, and $A_{1}, A_{2}, A_{3}, L$ the constants of $S$ .

Uses: Definition 4.2, Definition 4.1

Axiom (D1) is stated separately from the sieve datum because the same notion of density is also imposed level by level on the $N$ -indexed family of $W$ -tricked densities from which the constants $A_{2}$ and $L$ are extracted; the two uses share one definition rather than duplicating four axioms. Note also that (D2) forces $γ (p) \leq (1 - A_{1}) p$ uniformly in $p$ , which is strictly stronger than the pointwise inequality $γ (p) < p$ of (D1)(iv); both are recorded because the weaker one is what the construction of $g_{*}$ needs, and the stronger one is what the analytic estimates need.

Definition 4.4 (The derived multiplicative function $g_{*}$ ). Let $S = (γ, V, A_{1}, A_{2}, A_{3}, L)$ be a sieve datum (Definition 4.3). The derived function $g_{*} : N \to R$ is the totally multiplicative function determined by its prime values $g_{*} (p) := \frac{γ ( p )}{p - γ ( p )};$ explicitly, $g_{*} (n) := \prod_{p} g_{*} (p)^{v_{p} (n)}$ , where $v_{p} (n)$ is the exponent of $p$ in $n$ , so that $g_{*} (1) = 1$ .

Lean: PrimeGaps.SieveDatum.gStar

Uses: Definition 4.3

Lemma 4.5 ( $g_{*}$ is well defined and non-negative). Let $S$ be a sieve datum and $p$ a prime. Then $p - γ (p) > 0$ , and $g_{*} (p) \geq 0$ .

Lean: PrimeGaps.lem_g_star_well_defined

Uses: Definition 4.3, Definition 4.4

Proof. Axiom (D1)(iv) of Definition 4.3 gives $γ (p) < p$ , i.e. $p - γ (p) > 0$ ; hence the quotient defining $g_{*} (p)$ makes sense. (Axiom (D2) sharpens this to $p - γ (p) \geq A_{1} p$ , a bound uniform in $p$ , which is what the analytic applications use.) Since $γ (p) \geq 0$ by (D1)(i) and the denominator is positive, $g_{*} (p) = γ (p) / (p - γ (p)) \geq 0$ . ◻

Because $g_{*}$ is totally multiplicative and non-negative at every prime, $g_{*} (n) \geq 0$ for every $n$ , and on a squarefree $n$ one has $g_{*} (n) = \prod_{p ∣ n} g_{*} (p)$ . We use both facts freely below.

Definition 4.6 (The convolution summand $h$ ). Let $S$ be a sieve datum with derived function $g_{*}$ (Definition 4.4). Define $h : N \to R$ by $h (d) := μ (d)^{2} g_{*} (d) .$

Lean: PrimeGaps.SieveDatum.h

Uses: Definition 4.4, Definition 3.3

Lemma 4.7 ( $h$ is supported on integers coprime to the modulus). Let $S = (γ, V, A_{1}, A_{2}, A_{3}, L)$ be a sieve datum. If $d \geq 1$ satisfies $(d, V) > 1$ , then $h (d) = 0$ .

Uses: Definition 4.3, Definition 4.6, Definition 4.4

Proof. Since $(d, V) > 1$ , the integer $(d, V)$ has a prime divisor $p$ ; then $p ∣ d$ and $p ∣ V$ . By axiom (D3) of Definition 4.3, $γ (p) = 0$ ; by Lemma 4.5 the denominator $p - γ (p)$ is strictly positive, so Definition 4.4 gives $g_{*} (p) = 0/ (p - γ (p)) = 0$ . Write $d = p c$ with $c \geq 1$ . Total multiplicativity of $g_{*}$ gives $g_{*} (d) = g_{*} (p) g_{*} (c) = 0$ , whence $h (d) = μ (d)^{2} g_{*} (d) = 0$ . ◻

Proof uses: Lemma 4.5

Thus $h$ is a non-negative arithmetic function supported on the squarefree integers coprime to $V$ , and its partial sums are the input to the partial-summation lemma below. The next function records the deviation of $g_{*}$ from the model density $1/ (p - 1)$ at each prime not dividing the modulus.

Definition 4.8 (The convolution defect $b$ ). Let $S = (γ, V, A_{1}, A_{2}, A_{3}, L)$ be a sieve datum with derived function $g_{*}$ . Define $b : N \to R$ by $b (n) := ⎩ ⎨ ⎧ p ∣ n \prod (g_{*} (p) - \frac{1}{p - 1}), 0, if n is squarefree and (n, V) = 1, otherwise,$ the product being over the distinct primes dividing $n$ (so $b (1) = 1$ ).

Lean: PrimeGaps.SieveDatum.bDefect

Uses: Definition 4.3, Definition 4.4

By construction $b$ is multiplicative, vanishes off the squarefree integers coprime to $V$ , and takes the value $b (p) = g_{*} (p) - \frac{1}{p - 1} = \frac{γ ( p )}{p - γ ( p )} - \frac{1}{p - 1} = \frac{p ( γ ( p ) - 1 )}{( p - γ ( p )) ( p - 1 )}$ at a prime $p ∤ V$ ; axiom (D4) therefore makes $b (p)$ of size $O (1/ p^{2})$ .

We now record the density to which the construction is applied.

Definition 4.9 (The $W$ -tricked density $γ_{g}$ ). Let $V \geq 1$ . Define $γ_{g}^{(V)} : N \to R$ to be the totally multiplicative function with prime values $γ_{g}^{(V)} (p) := ⎩ ⎨ ⎧ 0, \frac{p}{p - 1}, p ∣ V, p ∤ V,$ that is, $γ_{g}^{(V)} (n) := \prod_{p} γ_{g}^{(V)} (p)^{v_{p} (n)}$ , with $v_{p} (n)$ the exponent of $p$ in $n$ .

Lemma 4.10 (The Maynard sieve datum). Let $V \geq 1$ be squarefree with $2 ∣ V$ , and suppose $A_{2} > 0$ and $L \geq 0$ are such that $- L \leq Δ (γ_{g}^{(V)}; w, z) \leq A_{2}$ for all real $2 \leq w \leq z$ . Let $S_{V}$ be the six-tuple $S_{V} = (γ_{g}^{(V)}, V, A_{1} = \frac{1}{2}, A_{2}, A_{3} = 2, L) .$ Then $S_{V}$ is a sieve datum in the sense of Definition 4.3.

Uses: Definition 4.3, Definition 4.9, Definition 4.1

Proof. Write $γ := γ_{g}^{(V)}$ . Axiom (D5) is the hypothesis, and the squarefreeness of $V$ together with $γ (p) = 0$ for $p ∣ V$ (immediate from Definition 4.9) is axiom (D3). We check the remaining axioms.

(D1) Density. Every prime value $γ (p)$ is non-negative — it is either $0$ or $p / (p - 1) > 0$ — so the product over the prime factorisation defining $γ (n)$ is non-negative, and $γ (1) = 1$ as an empty product. Total multiplicativity of $γ$ over prime factorisations gives $γ (mn) = γ (m) γ (n)$ for all coprime $m, n$ (indeed for all nonzero $m, n$ ). For (iv), if $p ∣ V$ then $γ (p) = 0 < p$ . If $p ∤ V$ , then $p \neq = 2$ because $2 ∣ V$ , so $p \geq 3$ ; and $p / (p - 1) < p$ is equivalent to $1 < p - 1$ , i.e. to $p > 2$ , which holds.

(D2) Growth with $A_{1} = 1/2$ . Certainly $0 < 1/2 < 1$ . If $p ∣ V$ then $γ (p) / p = 0 \leq 1/2$ . If $p ∤ V$ then $p \geq 3$ as above, and $γ (p) / p = 1/ (p - 1) \leq 1/2$ .

(D4) Unit density with $A_{3} = 2$ . Clearly $2 \geq 0$ . Let $p ∤ V$ . Then $∣ γ (p) - 1∣ = \frac{p}{p - 1} - 1 = \frac{1}{p - 1},$ and $1/ (p - 1) \leq 2/ p$ is equivalent to $p \leq 2 (p - 1)$ , i.e. to $p \geq 2$ , which holds for every prime. ◻

In the application $V$ is the primorial modulus $W$ of the $W$ -trick (Definition 3.29), which is squarefree and even as soon as $D_{0} (N) \geq 2$ ; the constants $A_{2}$ and $L$ are then supplied, uniformly in $N$ , by the Mertens estimates for the family $γ_{g}$ .

4.2 Tensor sieve coefficients

Notation 4.11 (Boldface $k$ -tuple convention). A boldface symbol such as $d$ denotes the $k$ -tuple of positive integers $(d_{1}, \dots, d_{k})$ , and we use the following conventions throughout.

$λ (d)$ denotes the value $λ (d_{1}, \dots, d_{k})$ . The bare symbol $λ$ denotes the function $N^{k} \to R$ itself (as when it is passed as an argument to $w_{n}$ , $S_{1}$ , $S_{2}$ or $S_{2}^{(m)}$ ); we never write a subscripted form such as $λ_{d}$ .
$\sum_{d}$ denotes the iterated sum $\sum_{d_{1}} \sum_{d_{2}} \dots \sum_{d_{k}}$ , each variable ranging over $N$ , and $\prod_{i} d_{i}$ the product $d_{1} d_{2} \dots d_{k}$ .
$\sum_{d_{i} ∣ n + h_{i} \forall i}$ abbreviates $\sum_{d_{1} ∣ n + h_{1}} \sum_{d_{2} ∣ n + h_{2}} \dots \sum_{d_{k} ∣ n + h_{k}}$ .
Analogous conventions apply to $e$ , $r$ , $u$ , $a$ , $b$ .

All the sieve coefficient functions occurring below are finitely supported: the set ${d : λ (d) \neq = 0}$ is finite. Every $d$ -sum written without further qualification is therefore a finite sum, and no convergence question arises.

The sieve coefficients are indexed by $k$ -tuples of divisors, one per shift $h_{i}$ , subject to three conditions: a truncation on the product of the divisors, coprimality to the $W$ -trick modulus, and squarefreeness of the product. The truncation level is carried as a parameter rather than fixed to $R^{1 + ε}$ , and every lemma below is stated once, at an arbitrary level.

Two consequences of (iii) are used constantly and without comment: each individual $d_{i}$ is squarefree (being a divisor of the squarefree $\prod_{i} d_{i}$ ), and the $d_{i}$ are pairwise coprime. Throughout, $λ$ has permissible support at level $T = ⌊ R^{1 + ε} ⌋$ .

4.3 The sieve weights and the sums $S_{1} (λ)$ , $S_{2} (λ)$

Definition 4.12 (Sieve weight). Let $λ : N^{k} \to R$ be finitely supported and let $n \geq 1$ be an integer. The sieve weight at $n$ is $w_{n} := (d_{i} ∣ n + h_{i} \forall i \sum λ (d_{1}, \dots, d_{k}))^{2} .$

Lean: PrimeGaps.termW, PrimeGaps.weight

Uses: Notation 4.11

Lemma 4.13 (Non-negativity of $w_{n}$ ). For every finitely supported $λ : N^{k} \to R$ and every integer $n \geq 1$ , we have $w_{n} \geq 0$ .

Lean: PrimeGaps.w_nonneg

Uses: Definition 4.12

Proof. By Definition 4.12, $w_{n}$ is the square of the real number $\sum_{d_{i} ∣ n + h_{i} \forall i} λ (d)$ , and squares of real numbers are non-negative. ◻

Non-negativity of $w_{n}$ is the only property of the weight used in the passage from positivity of the sieve sums to primes; everything else about $w_{n}$ enters through the asymptotic evaluation of $S_{1}$ and $S_{2}$ .

Definition 4.14 (The sum $S_{1} (λ)$ ). Let $λ : N^{k} \to R$ be finitely supported, with sieve weight $w_{n}$ as in Definition 4.12. Set $S_{1} (λ) := N < n \leq 2 N n \equiv v_{0} (mod W) \sum w_{n} .$

Lean: PrimeGaps.S₁

Uses: Definition 4.12, Definition 3.29, Definition 3.33

Definition 4.15 (The sum $S_{2} (λ)$ ). Let $λ : N^{k} \to R$ be finitely supported, with sieve weight $w_{n}$ as in Definition 4.12. Set $S_{2} (λ) := N < n \leq 2 N n \equiv v_{0} (mod W) \sum (i = 1 \sum k χ_{P} (n + h_{i})) w_{n},$ so that each $n$ is weighted by the number of indices $i$ for which $n + h_{i}$ is prime.

Lean: PrimeGaps.S₂

Uses: Definition 4.12, Definition 3.29, Definition 3.33

Definition 4.16 (The sum $S_{2}^{(m)} (λ)$ ). Let $m \in {1, \dots, k}$ and let $λ : N^{k} \to R$ be finitely supported, with sieve weight $w_{n}$ as in Definition 4.12. Set $S_{2}^{(m)} (λ) := N < n \leq 2 N n \equiv v_{0} (mod W) \sum χ_{P} (n + h_{m}) w_{n} .$

Lean: PrimeGaps.S₂m

Uses: Definition 4.12, Definition 3.29, Definition 3.33

Lemma 4.17 (Decomposition of $S_{2} (λ)$ ). For every finitely supported $λ : N^{k} \to R$ , $S_{2} (λ) = m = 1 \sum k S_{2}^{(m)} (λ) .$

Lean: PrimeGaps.sum_S₂m_eq_S₂

Uses: Definition 4.15, Definition 4.16

Proof. Fix $n$ in the index set of Definition 4.15. Distributing the finite inner sum across the product with $w_{n}$ gives $(i = 1 \sum k χ_{P} (n + h_{i})) w_{n} = i = 1 \sum k χ_{P} (n + h_{i}) w_{n} .$ Substituting this into Definition 4.15 and interchanging the two finite summations — over $n \in (N, 2 N]$ with $n \equiv v_{0} (mod W)$ , and over $i \in {1, \dots, k}$ — yields $S_{2} (λ) = i = 1 \sum k N < n \leq 2 N n \equiv v_{0} (mod W) \sum χ_{P} (n + h_{i}) w_{n} .$ By Definition 4.16 the inner sum is exactly $S_{2}^{(i)} (λ)$ ; renaming the index $i$ to $m$ gives the claim. ◻

Definition 4.18 (The sieve difference $S (λ, ρ)$ ). Let $λ : N^{k} \to R$ be finitely supported and let $ρ > 0$ be real. Set $S (λ, ρ) := S_{2} (λ) - ρ S_{1} (λ) .$

Uses: Definition 4.14, Definition 4.15

Unwinding Definitions 4.14 and 4.15, the sieve difference is the single sum $S (λ, ρ) = N < n \leq 2 N n \equiv v_{0} (mod W) \sum (i = 1 \sum k χ_{P} (n + h_{i}) - ρ) w_{n},$ whose summands are the weights $w_{n} \geq 0$ multiplied by the excess of the prime count over $ρ$ . Positivity of $S (λ, ρ)$ therefore cannot come from the weights alone; it forces the excess to be positive somewhere. This is the GPY reduction, and it is the sole point at which the sieve produces primes.

Lemma 4.19. Let $λ : N^{k} \to R$ be finitely supported and let $ρ > 0$ . If $S (λ, ρ) > 0$ , then there exists an integer $n$ with $N < n \leq 2 N$ and $n \equiv v_{0} (mod W)$ such that at least $⌊ ρ + 1 ⌋$ of $n + h_{1}, \dots, n + h_{k}$ are prime.

Lean: PrimeGaps.lem_S_positive_implies_primes

Uses: Definition 4.18, Definition 4.14, Definition 4.15, Definition 4.12, Definition 3.29, Lemma 3.34

Proof. Write $c (n) := # {i \in {1, \dots, k} : n + h_{i} \in P} = \sum_{i = 1}^{k} χ_{P} (n + h_{i})$ , so that, as computed above, $S (λ, ρ) = N < n \leq 2 N n \equiv v_{0} (mod W) \sum (c (n) - ρ) w_{n} .$ Suppose, for contradiction, that $c (n) \leq ρ$ for every $n$ in the index set. By Lemma 4.13 each $w_{n} \geq 0$ , so each summand $(c (n) - ρ) w_{n}$ is non-positive, and therefore $S (λ, ρ) \leq 0$ , contradicting the hypothesis. Hence there is an $n$ in the index set with $c (n) > ρ$ .

It remains to convert $c (n) > ρ$ into $c (n) \geq ⌊ ρ + 1 ⌋$ . Since $c (n)$ is an integer and $c (n) > ρ$ , we have $c (n) \geq ⌊ ρ ⌋ + 1$ when $ρ \in / Z$ , and $c (n) \geq ρ + 1$ when $ρ \in Z$ ; in either case $c (n) \geq ⌊ ρ + 1 ⌋$ , because $⌊ ρ + 1 ⌋ = ⌊ ρ ⌋ + 1$ . ◻

Proof uses: Lemma 4.13

4.4 The auxiliary $y$ -variables

The coefficients $λ (d)$ are natural for the divisor-sum manipulations of $S_{1}$ and $S_{2}$ , but ill-suited as variational unknowns: the divisibility relations couple them, and the diagonal form of the sieve sums is not visible in them. The change of variables $λ \leftrightarrow y$ below is a linear, involutive Möbius-type substitution which diagonalises $S_{1}$ and, after a further substitution $y ⇝ y^{(m)}$ , also $S_{2}^{(m)}$ . We give here the definitions and the inversion identities; the asymptotic evaluation of $S_{1}$ and $S_{2}^{(m)}$ in terms of $y$ and $y^{(m)}$ is carried out later.

Definition 4.20 (The $y$ -transform $y_{λ}$ of $λ$ ). Let $λ : N^{k} \to R$ be finitely supported. Define $y_{λ} : N^{k} \to R$ by $y_{λ} (r_{1}, \dots, r_{k}) := (i = 1 \prod k μ (r_{i}) φ (r_{i})) d \in N^{k} r_{i} ∣ d_{i} and d_{i} squarefree \forall i \sum \frac{λ ( d _{1} , \dots , d _{k} )}{\prod _{i = 1}^{k} d _{i}} .$ The $d$ -sum is finite because $λ$ is finitely supported, and $y_{λ}$ is again finitely supported. We write $y := y_{λ}$ and call its values the $y$ -variables of $λ$ .

Lean: PrimeGaps.lToY, PrimeGaps.lToY_apply, PrimeGaps.lToY_apply'

Uses: Definition 3.3, Definition 3.4, Notation 4.11

The squarefreeness restriction on the summation variables is vacuous in every application: if $λ$ has permissible support at some level, then each $d_{i}$ in its support is squarefree by Definition 3.39(iii), and the sum reduces to the unrestricted $\sum_{r_{i} ∣ d_{i} \forall i}$ . Carrying the restriction in the definition lets the inversion identities below hold for arbitrary finitely supported $λ$ , with no support hypothesis; the map $λ \mapsto y_{λ}$ is $R$ -linear.

Lemma 4.21 (The $y$ -variables inherit permissible support). Let $T \geq 1$ and let $λ : N^{k} \to R$ have permissible support at level $T$ (Definition 3.39). Then $y_{λ}$ has permissible support at level $T$ .

Lean: Finsupp.HasPermissibleSupport.lToY

Uses: Definition 3.39, Definition 4.20

Proof. Suppose $y_{λ} (r) \neq = 0$ . Then some summand of the defining sum in Definition 4.20 is nonzero, so there is a $d$ with $λ (d) \neq = 0$ and $r_{i} ∣ d_{i}$ for every $i$ . It therefore suffices to show that the three conditions of Definition 3.39 are inherited from $d$ to any coordinatewise divisor $r$ of $d$ . That is exactly Lemma 3.40, applied at level $T$ .

In detail: since $r_{i} ∣ d_{i}$ for each $i$ , we have $\prod_{i} r_{i} ∣ \prod_{i} d_{i}$ . As all $d_{i}$ are nonzero, $\prod_{i} d_{i} \geq 1$ and hence $\prod_{i} r_{i} \leq \prod_{i} d_{i} \leq T$ , which is (i). A divisor of an integer coprime to $W$ is coprime to $W$ , giving (ii); and a divisor of a squarefree integer is squarefree, giving (iii). ◻

Proof uses: Lemma 3.40

Definition 4.22 (The Möbius transform $λ_{y}$ of $y$ ). Let $y : N^{k} \to R$ be finitely supported. Define $λ_{y} : N^{k} \to R$ by $λ_{y} (d_{1}, \dots, d_{k}) := (i = 1 \prod k μ (d_{i}) d_{i}) r \in N^{k} d_{i} ∣ r_{i} and r_{i} squarefree \forall i \sum \frac{y ( r _{1} , \dots , r _{k} )}{\prod _{i = 1}^{k} φ ( r _{i} )} .$ The $r$ -sum is finite because $y$ is finitely supported, and $λ_{y}$ is again finitely supported.

Lean: PrimeGaps.yToL, PrimeGaps.yToL_apply, PrimeGaps.yToL_apply'

Uses: Definition 3.3, Definition 3.4, Notation 4.11

The transform $y \mapsto λ_{y}$ is $R$ -linear, and the argument of Lemma 4.21 applies verbatim (with the roles of $d$ and $r$ exchanged) to show that it too preserves permissible support at any level $T$ . The next two lemmas identify the two transforms as inverses.

Lemma 4.23 (Möbius inversion: $λ$ from $y$ ). Let $λ : N^{k} \to R$ be finitely supported, and let $y : N^{k} \to R$ satisfy $y = y_{λ}$ (Definition 4.20). Then for every $d \in N^{k}$ , $λ_{y} (d_{1}, \dots, d_{k}) = {λ (d_{1}, \dots, d_{k}), 0, if every d_{i} is squarefree, otherwise .$

Lean: PrimeGaps.yToL_lToY

Uses: Definition 4.20, Definition 4.22, Definition 3.3, Definition 3.4

Proof. If some $d_{i}$ is not squarefree, then every $r$ contributing to Definition 4.22 has $d_{i} ∣ r_{i}$ with $r_{i}$ squarefree, forcing $d_{i}$ squarefree — a contradiction. So the sum is empty and $λ_{y} (d) = 0$ . Assume henceforth that every $d_{i}$ is squarefree.

Both transforms are $R$ -linear in their argument, and every finitely supported function is a finite linear combination of point masses; so it suffices to prove the identity when $λ = c \cdot 1_{d^{(0)}}$ is a point mass at some $d^{(0)}$ with weight $c$ . For such $λ$ , $y (r) = (i \prod μ (r_{i}) φ (r_{i})) \frac{c}{\prod _{i} d _{i}^{(0)}} if r_{i} ∣ d_{i}^{(0)} and d_{i}^{(0)} is squarefree for all i,$ and $y (r) = 0$ otherwise; in particular $y$ is supported on the coordinatewise divisors of $d^{(0)}$ . If some $d_{i}^{(0)}$ fails to be squarefree, or if $d_{i} ∤ d_{i}^{(0)}$ for some $i$ , then no $r$ contributes to $λ_{y} (d)$ and both sides vanish (on the right, $λ (d) = 0$ unless $d = d^{(0)}$ , and the excluded cases exclude that). Otherwise substitute the displayed formula for $y$ into Definition 4.22: the factors $φ (r_{i})$ cancel, and $λ_{y} (d) = \frac{c \prod _{i} μ ( d _{i} ) d _{i}}{\prod _{i} d _{i}^{(0)}} r d_{i} ∣ r_{i} ∣ d_{i}^{(0)} \forall i \sum i = 1 \prod k μ (r_{i}) = \frac{c \prod _{i} μ ( d _{i} ) d _{i}}{\prod _{i} d _{i}^{(0)}} i = 1 \prod k (d_{i} ∣ r_{i} ∣ d_{i}^{(0)} \sum μ (r_{i})),$ the sum having factorised across coordinates. For squarefree $d_{i}^{(0)}$ the inner sum is $μ (d_{i}) 1 [d_{i} = d_{i}^{(0)}]$ , by Möbius inversion applied to the divisor chain $d_{i} ∣ r_{i} ∣ d_{i}^{(0)}$ (writing $r_{i} = d_{i} s_{i}$ with $s_{i} ∣ d_{i}^{(0)} / d_{i}$ and using $μ (d_{i} s_{i}) = μ (d_{i}) μ (s_{i})$ , valid since $d_{i}^{(0)}$ is squarefree, together with $\sum_{s ∣ t} μ (s) = 1 [t = 1]$ ). Hence the whole expression vanishes unless $d = d^{(0)}$ , in which case it equals $\frac{c \prod _{i} μ ( d _{i} ) d _{i}}{\prod _{i} d _{i}} i \prod μ (d_{i}) = c i \prod μ (d_{i})^{2} = c,$ because each $d_{i}$ is squarefree. This is $λ (d)$ , as required. ◻

Lemma 4.24 (Möbius inversion: $y$ from $λ$ ). Let $y : N^{k} \to R$ be finitely supported and let $λ_{y}$ be as in Definition 4.22. Then for every $r \in N^{k}$ , $y_{λ_{y}} (r_{1}, \dots, r_{k}) = {y (r_{1}, \dots, r_{k}), 0, if every r_{i} is squarefree, otherwise .$

Lean: PrimeGaps.lToY_yToL

Uses: Definition 4.20, Definition 4.22, Definition 3.3, Definition 3.4

Proof. The argument is that of Lemma 4.23 with the roles of the two transforms exchanged. If some $r_{i}$ is not squarefree, every $d$ contributing to Definition 4.20 at $r$ has $r_{i} ∣ d_{i}$ with $d_{i}$ squarefree, which is impossible; so $y_{λ_{y}} (r) = 0$ . Assume every $r_{i}$ squarefree. By linearity reduce to $y = c \cdot 1_{r^{(0)}}$ a point mass. Then $λ_{y}$ is supported on the coordinatewise divisors of $r^{(0)}$ , and substituting Definition 4.22 into Definition 4.20 the factors $d_{i}$ cancel against $1/ \prod_{i} d_{i}$ , leaving $y_{λ_{y}} (r) = \frac{c \prod _{i} μ ( r _{i} ) φ ( r _{i} )}{\prod _{i} φ ( r _{i}^{(0)} )} i = 1 \prod k (r_{i} ∣ d_{i} ∣ r_{i}^{(0)} \sum μ (d_{i})) .$ As before each inner sum equals $μ (r_{i}) 1 [r_{i} = r_{i}^{(0)}]$ , so the expression vanishes unless $r = r^{(0)}$ , and then equals $c \prod_{i} μ (r_{i})^{2} = c = y (r)$ . ◻

Proof uses: Lemma 4.23

Together, Lemmas 4.23 and 4.24 say that the two transforms are mutually inverse $R$ -linear isomorphisms of the space of finitely supported functions $N^{k} \to R$ that vanish at every tuple with some non-squarefree entry. In particular one may specify a sieve either by giving $λ$ or by giving $y$ ; the second is the form used in the variational problem.

The analysis of $S_{2}^{(m)}$ requires a second, closely related transform, in which the $m$ -th coordinate is frozen at $1$ and the totient $φ$ is replaced by the function $g$ defined next.

On squarefree arguments — the only ones at which $g$ is ever evaluated below, since it always occurs multiplied by $μ$ — one has $g (n) = \prod_{p ∣ n} (p - 2)$ .

Definition 4.25 (The $y^{(m)}$ -variables). Let $m \in {1, \dots, k}$ and let $λ : N^{k} \to R$ be finitely supported. Define $y^{(m)} : N^{k} \to R$ by $y^{(m)} (r_{1}, \dots, r_{k}) := (i = 1 \prod k μ (r_{i}) g (r_{i})) d \in N^{k}, d_{m} = 1 r_{i} ∣ d_{i} and d_{i} squarefree \forall i \sum \frac{λ ( d _{1} , \dots , d _{k} )}{\prod _{i = 1}^{k} φ ( d _{i} )} .$

Lean: PrimeGaps.ym, PrimeGaps.ym_apply, PrimeGaps.ym_apply'

Uses: Definition 3.3, Definition 3.6, Definition 3.4, Notation 4.11

Because $μ (1) = g (1) = φ (1) = 1$ , the factors carrying the index $m$ contribute trivially: the prefactor may equally be written $\prod_{i \neq = m} μ (r_{i}) g (r_{i})$ and the denominator $\prod_{i \neq = m} φ (d_{i})$ , which is the shape in which $y^{(m)}$ appears in the evaluation of $S_{2}^{(m)}$ .

Lemma 4.26 (Support of $y^{(m)}$ ). Let $m \in {1, \dots, k}$ and $λ : N^{k} \to R$ finitely supported. If $y^{(m)} (r_{1}, \dots, r_{k}) \neq = 0$ , then $r_{m} = 1$ .

Lean: PrimeGaps.eq_one_of_ym_ne_zero

Uses: Definition 4.25

Proof. If $y^{(m)} (r) \neq = 0$ then the defining sum of Definition 4.25 has a nonzero summand, so there is a $d$ with $d_{m} = 1$ and $r_{i} ∣ d_{i}$ for every $i$ . Taking $i = m$ gives $r_{m} ∣ 1$ , hence $r_{m} = 1$ . ◻

Finally we record the coefficient function that the two instantiations use in $S_{1}$ and $S_{2}$ . It is specified in the $y$ -variables — a rescaled sample of a fixed function $F$ on the truncation scale — and the corresponding $λ$ is produced by the Möbius transform of Definition 4.22. The analytic input is $F$ , and $λ$ is the derived object.

By construction $y_{0}$ has permissible support at level $T$ , hence is finitely supported, so Definition 4.22 applies to it.

Since the Möbius transform preserves permissible support, $λ_{0}$ has permissible support at level $T$ , so all of Definitions 4.12–4.18 apply to it. We take $T = ⌊ R^{1 + ε} ⌋$ with $F$ supported in the enlarged simplex $T_{ε}$ .

Definition 4.27 (Maximal modulus of a finitely supported system). Let $A$ be a set and let $f : A \to R$ be finitely supported. Its maximal modulus is $∥ f ∥_{m a x} := a \in supp f max ∣ f (a) ∣,$ with the convention $∥ f ∥_{m a x} := 0$ when $f$ vanishes identically.

Lean: Finsupp.le_maxRealAbs, Finsupp.maxRealAbs, Finsupp.maxRealAbs_le_iff

Definition 4.28 (The truncated weight sum $H (z)$ ). Let $S$ be a sieve datum with associated weight $h$ (Definition 4.6). For a real $z > 0$ set $H (z) := 0 < d < z \sum h (d),$ the sum taken over positive integers $d$ strictly below $z$ .

Lean: PrimeGaps.SieveDatum.H

Uses: Definition 4.6

Definition 4.29 (The Maynard sieve datum). Let $N$ be a positive integer with $2 \leq D_{0} (N)$ . The Maynard sieve datum at $N$ is the sieve datum (Definition 4.3) whose density is the $W$ -tricked density $γ_{g}$ of Definition 4.9, whose modulus is $V := W$ , and whose growth and structure constants are $A_{1} := 1/2$ and $A_{3} := 2$ . Its remaining constants $A_{2}$ and $L$ are the deviation bounds carried by the datum; that they may be taken uniformly in $N$ is established in Section 6.

Lean: PrimeGaps.maynardSieveDatum

Uses: Definition 4.3, Definition 3.29, Definition 4.9

5 The variational problem

The sieve estimates of the preceding sections reduce the problem to one in the calculus of variations. A profile $F$ supported on a simplex determines the sieve coefficients $λ$ ; the leading term of $S_{1} (λ)$ is the $L^{2}$ mass $I_{k} (F)$ of the profile, and the leading term of $S_{2}^{(m)} (λ)$ is the $L^{2}$ mass $J_{k, ε}^{(m)} (F)$ of its $m$ -th marginal. The supremum of the ratio $(\sum_{m} J_{k, ε}^{(m)} (F)) / I_{k} (F)$ over profiles $F$ is the constant $M_{k, ε}$ .

The construction is carried out for an enlargement parameter $ε \geq 0$ . The profile is supported on the enlarged simplex $T_{ε}$ of total mass $1 + ε$ , while each marginal is taken over the shrunken slice $S_{ε}$ of total mass $1 - ε$ ; at $ε = 0$ both reduce to the standard simplex and its faces, and every statement below specialises to the classical one. The denominator $I_{k} (F) = \int F^{2}$ does not depend on $ε$ ; the enlargement enters only through the wider class of admissible competitors.

We introduce $T_{ε}$ , $F$ , $I_{k}$ , $J_{k, ε}^{(m)}$ and $M_{k, ε}$ , and record the properties of $M_{k, ε}$ used below: the $L^{2}$ -continuity of the two functionals, and the density of smooth profiles. The remaining lemmas evaluate integrals of monomials over the scaled standard simplex.

5.1 The simplex and the profile

Definition 5.1 (Scaled standard simplex). Let $k \in Z_{\geq 0}$ and $s \in R$ . The scaled standard simplex of dimension $k$ and scale $s$ is $R_{k} (s) := {t = (t_{1}, \dots, t_{k}) \in R^{k} : t_{i} \geq 0 for every i, i = 1 \sum k t_{i} \leq s} .$ Three instances recur, and we abbreviate them. For $ε \geq 0$ : $R_{k} T_{ε} S_{ε} := := := R_{k} (1), R_{k} (1 + ε), R_{k - 1} (1 - ε),$ called respectively the standard simplex, the $ε$ -enlarged simplex and the $ε$ -shrunken slice. Thus $T_{0} = R_{k}$ and $S_{0} = R_{k - 1}$ ; we also write $R_{k}^{(m)}$ for the copy of $R_{k - 1}$ obtained by deleting the $m$ -th coordinate of $R^{k}$ , so that $S_{0} = R_{k}^{(m)}$ under that identification.

Lean: EuclideanSpace.mem_scaledStdSimplex_iff, PrimeGaps.term𝓡_

5.2 The functionals $I_{k}$ , $J_{k, ε}^{(m)}$ and the constant $M_{k, ε}$

Definition 5.2 (The functional $I_{k}$ ). For $k \in N$ and $F \in L^{2} (R^{k})$ , $I_{k} (F) := \int_{R^{k}} F (t_{1}, \dots, t_{k})^{2} d t_{1} \dots d t_{k} .$ If $F$ vanishes outside a measurable set $S$ then $I_{k} (F) = \int_{S} F^{2} = ∥ F ∥_{L^{2} (S)}^{2}$ ; in particular $I_{k} (F) = ∥ F ∥_{L^{2} (T_{ε})}^{2}$ for a profile supported in $T_{ε}$ . The functional carries no dependence on $ε$ .

Uses: Definition 5.1

Definition 5.3 (The marginal functional $J_{k, ε}^{(m)}$ ). Let $k \geq 1$ , let $ε \geq 0$ , let $m \in {1, \dots, k}$ , and let $F : R^{k} \to R$ vanish outside $T_{ε}$ . Write $T_{m}$ for the $m$ -th marginal operator $(T_{m} F) (t_{1}, \dots, t_{m}, \dots, t_{k}) := \int_{0}^{\infty} F (t_{1}, \dots, t_{k}) d t_{m},$ defined for almost every $(t_{i})_{i \neq = m} \in R^{k - 1}$ , and set $J_{k, ε}^{(m)} (F) := \int_{S_{ε}} (T_{m} F)^{2} i \neq = m \prod d t_{i} = ∥ T_{m} F ∥_{L^{2} (S_{ε})}^{2} .$ We abbreviate $J_{k}^{(m)} := J_{k, 0}^{(m)}$ , the marginal functional of the standard problem, whose outer domain $S_{0}$ is $R_{k}^{(m)}$ .

Lean: PrimeGaps.J, PrimeGaps.JBilinCLM

Uses: Definition 5.1

Definition 5.4 (The variational constant $M_{k, ε}$ ). For $k \geq 1$ and $ε \geq 0$ , $M_{k, ε} := sup {\frac{\sum _{m = 1}^{k} J _{k, ε}^{(m)} ( F )}{I _{k} ( F )} F \in L^{2} (T_{ε}), I_{k} (F) \neq = 0} .$ The supremum is taken over the whole of $L^{2} (T_{ε})$ , each competitor being extended by zero outside $T_{ε}$ : no smoothness, no symmetry and no sign condition is imposed on $F$ . We abbreviate $M_{k} := M_{k, 0}$ .

Lean: PrimeGaps.M

Uses: Definition 5.2, Definition 5.3

5.3 From a profile to the sieve coefficients

Definition 5.5 (The $y$ -variables attached to a profile). Let $k \in N$ , let $R > 1$ and $W \in N$ , and let $F : R^{k} \to R$ . Define $y_{0} : N^{k} \to R$ by $y_{0} (r_{1}, \dots, r_{k}) := ⎩ ⎨ ⎧ F (\frac{lo g r _{1}}{lo g R}, \dots, \frac{lo g r _{k}}{lo g R}), 0, (r_{1}, \dots, r_{k}) admissible for (R, W), otherwise,$ where a tuple is admissible for $(R, W)$ in the sense of Definition 3.39, i.e. $\prod_{i} r_{i} \leq R$ , $g cd (\prod_{i} r_{i}, W) = 1$ and $\prod_{i} r_{i}$ is squarefree.

Lean: PrimeGaps.y₀, PrimeGaps.y₀_apply

Uses: Definition 3.39

Definition 5.6 (The sieve coefficients attached to a profile). With $k$ , $R$ , $W$ and $F$ as in Definition 5.5, the coefficients $λ_{0} : N^{k} \to R$ attached to $F$ are the image of $y_{0}$ under the $y \mapsto λ$ correspondence of Definition 4.22: $λ_{0} (d_{1}, \dots, d_{k}) = (i = 1 \prod k μ (d_{i}) d_{i}) (r_{1}, \dots, r_{k}) admissible for (R, W) d_{i} ∣ r_{i} for every i \sum \frac{y _{0} ( r _{1} , \dots , r _{k} )}{\prod _{i = 1}^{k} φ ( r _{i} )} .$ Taking $F$ supported in $T_{ε}$ and truncation level $R^{1 + ε}$ produces the enlarged weight; taking $F$ supported in $R_{k}$ and level $R$ produces the standard one.

Lean: PrimeGaps.l₀_apply

Uses: Definition 5.5, Definition 4.22, Definition 3.39, Definition 5.1

5.4 Basic properties of $I_{k}$ , $J_{k, ε}^{(m)}$ and $M_{k, ε}$

Lemma 5.7 (Each marginal is dominated by the $L^{2}$ mass). Let $k \geq 1$ , let $ε \geq 0$ , let $F \in L^{2} (T_{ε})$ and let $m \in {1, \dots, k}$ . Then $J_{k, ε}^{(m)} (F) \leq (1 + ε) I_{k} (F) .$

Uses: Definition 5.2, Definition 5.3, Definition 5.1

Proof. Fix $(t_{i})_{i \neq = m} \in S_{ε}$ and consider the fibre $E := {s \geq 0 : (t_{1}, \dots, t_{m - 1}, s, t_{m + 1}, \dots, t_{k}) \in T_{ε}} .$ Since every $t_{i} \geq 0$ , the fibre is the interval $[0, 1 + ε - \sum_{i \neq = m} t_{i}]$ (empty if the right endpoint is negative), whose length is at most $1 + ε$ . Since $F$ vanishes off $T_{ε}$ , the Cauchy–Schwarz inequality on $E$ gives $(T_{m} F) ((t_{i})_{i \neq = m})^{2} = \int_{E} F d s^{2} \leq ∣ E ∣ \int_{E} F^{2} d s \leq (1 + ε) \int_{E} F^{2} d s .$ Integrating over $(t_{i})_{i \neq = m} \in S_{ε}$ and applying Tonelli’s theorem to the right-hand side, the iterated integral is bounded by the integral of $F^{2}$ over all of $R^{k}$ , which is $I_{k} (F)$ . Hence $J_{k, ε}^{(m)} (F) \leq (1 + ε) I_{k} (F)$ .

Equivalently: $T_{m}$ is a bounded linear operator $L^{2} (T_{ε}) \to L^{2} (S_{ε})$ whose norm is at most the square root of the essential supremum of the fibre lengths, and that essential supremum is at most $1 + ε$ . ◻

Lemma 5.8 ( $L^{2}$ -continuity of $I_{k}$ ). For every $ε \geq 0$ the functional $I_{k} : L^{2} (T_{ε}) \to R$ is continuous.

Lean: continuous_norm

Uses: Definition 5.2, Definition 5.1

Proof. On $L^{2} (T_{ε})$ we have $I_{k} (F) = ∥ F ∥_{L^{2} (T_{ε})}^{2}$ by Definition 5.2, so $I_{k}$ is the square of the norm, and the norm on a normed space is continuous. Quantitatively, for $F, G \in L^{2} (T_{ε})$ the factorisation $F^{2} - G^{2} = (F - G) (F + G)$ together with Cauchy–Schwarz and the triangle inequality gives $∣ I_{k} (F) - I_{k} (G) ∣ \leq ∥ F - G ∥ ∥ F + G ∥ \leq (∥ F ∥ + ∥ G ∥) ∥ F - G ∥,$ all norms being those of $L^{2} (T_{ε})$ . ◻

Lemma 5.9 ( $L^{2}$ -continuity of $J_{k, ε}^{(m)}$ ). For every $k \geq 1$ , every $ε \geq 0$ and every $m \in {1, \dots, k}$ , the functional $J_{k, ε}^{(m)} : L^{2} (T_{ε}) \to R$ is continuous.

Lean: PrimeGaps.continuous_J, PrimeGaps.continuous_JEps

Uses: Definition 5.3, Definition 5.1

Proof. The marginal operator $T_{m}$ is linear, and by the proof of Lemma 5.7 it is bounded from $L^{2} (T_{ε})$ to $L^{2} (S_{ε})$ , with norm at most $(1 + ε)^{1/2}$ ; hence it is continuous. The map $H \mapsto ∥ H ∥_{L^{2} (S_{ε})}^{2}$ is continuous, being the square of a norm. By Definition 5.3, $J_{k, ε}^{(m)}$ is the composite of these two continuous maps. Quantitatively, the argument of Lemma 5.8 applied in $L^{2} (S_{ε})$ together with the operator bound gives $J_{k, ε}^{(m)} (F) - J_{k, ε}^{(m)} (G) \leq (1 + ε) (∥ F ∥ + ∥ G ∥) ∥ F - G ∥$ with the norms of $L^{2} (T_{ε})$ . ◻

Proof uses: Lemma 5.7, Lemma 5.8

5.5 Smooth profiles and the variational criterion

The sieve asymptotics for $S_{1}$ and $S_{2}^{(m)}$ require a smooth profile supported in $T_{ε}$ , whereas $M_{k, ε}$ is a supremum over all of $L^{2} (T_{ε})$ . Smooth functions supported in the simplex are $L^{2}$ -dense there, hence (by the continuity of $I_{k}$ and $J_{k, ε}^{(m)}$ ) they realise the supremum to within any prescribed error, and the resulting near-maximiser satisfies the strict inequality required by the sieve estimates. The density statement is proved on the standard simplex and transported to $T_{ε}$ by the dilation $t \mapsto (1 + ε)^{- 1} t$ , which carries $T_{ε}$ onto $R_{k}$ .

Lemma 5.10 (Smooth cut-off to an inset of $R_{k}$ ). Let $k \geq 2$ and let $η$ satisfy $0 < η < 1/ (2 k)$ . There exists a smooth function $χ : R^{k} \to [0, 1]$ such that

$χ (t) = 1$ for every $t \in R_{k}$ satisfying $t_{i} \geq η$ for all $i$ and $\sum_{i} t_{i} \leq 1 - η$ ;
$χ (t) = 0$ for every $t \in / R_{k}$ ;
for every measurable $G : R^{k} \to R$ and every $M \geq 0$ with $∣ G ∣ \leq M$ on $R_{k}$ , $\int_{R_{k}} (G - G χ)^{2} \leq M^{2} vol ({t \in R_{k} : t_{i} < η for some i or i \sum t_{i} > 1 - η}) \leq M^{2} \cdot 2 k η .$

Lean: PrimeGaps.exists_smooth_simplex_cutoff

Uses: Definition 5.1

Proof. Fix a smooth non-decreasing $ψ : R \to [0, 1]$ with $ψ (u) = 0$ for $u \leq 0$ and $ψ (u) = 1$ for $u \geq 1$ , and put $ψ_{η} (u) := ψ (u / η)$ . Set $χ (t_{1}, \dots, t_{k}) := (i = 1 \prod k ψ_{η} (t_{i})) \cdot ψ_{η} (1 - i = 1 \sum k t_{i}) .$ This is a finite product of smooth functions, hence smooth, with values in $[0, 1]$ .

(i) If $t \in R_{k}^{(η)}$ then $t_{i} \geq η$ for each $i$ and $\sum_{i} t_{i} \leq 1 - η$ , so every factor equals $1$ .

(ii) If $t \in / R_{k}$ then either $t_{i} < 0$ for some $i$ , or $\sum_{i} t_{i} > 1$ ; in the first case $ψ_{η} (t_{i}) = 0$ and in the second $ψ_{η} (1 - \sum_{i} t_{i}) = 0$ .

(iii) On $R_{k}^{(η)}$ we have $G - G χ = 0$ by (i), while on all of $R_{k}$ we have $∣ G - G χ ∣ = ∣ G ∣ ∣1 - χ ∣ \leq M$ . Hence $\int_{R_{k}} (G - G χ)^{2} = \int_{R_{k} ∖ R_{k}^{(η)}} (G - G χ)^{2} \leq M^{2} vol (R_{k} ∖ R_{k}^{(η)}) .$ For the second inequality, $R_{k} ∖ R_{k}^{(η)}$ is covered by the $k$ slabs ${t \in R_{k} : t_{i} < η}$ together with the slab ${t \in R_{k} : \sum_{i} t_{i} > 1 - η}$ . Each of the first $k$ slabs has volume at most $η / (k - 1)!$ , since its cross-section at fixed $t_{i}$ lies in a $(k - 1)$ -dimensional simplex of volume $1/ (k - 1)!$ ; the last slab, being the difference of two simplices, has volume $(1 - (1 - η)^{k}) / k! \leq η / (k - 1)!$ . Summing gives $vol (R_{k} ∖ R_{k}^{(η)}) \leq (k + 1) η / (k - 1)! \leq 2 k η$ for $k \geq 2$ . ◻

Lemma 5.11 ( $L^{2}$ -density of smooth functions supported in $R_{k}$ ). Let $k \geq 2$ , let $F_{0} \in L^{2} (R_{k})$ and let $δ > 0$ . Then there exists a smooth $F_{1} : R^{k} \to R$ whose closed support is contained in $R_{k}$ and which satisfies $∥ F_{0} - F_{1} ∥_{L^{2} (R_{k})} < δ .$

Lean: PrimeGaps.smooth_L2_approx_on_simplex

Uses: Definition 5.1

Proof. Extend $F_{0}$ by zero to $R^{k}$ ; the extension lies in $L^{2} (R^{k})$ with the same norm. By the density of smooth compactly supported functions in $L^{2} (R^{k})$ there is a smooth compactly supported $F$ with $∥ F_{0} - F ∥_{L^{2} (R^{k})} < δ /3$ ; restricting the integration to $R_{k}$ only decreases the left-hand side. Being continuous with compact support, $F$ is bounded on $R_{k}$ ; let $M \geq 0$ be a bound for $∣ F ∣$ there.

Choose $η \in (0, 1/ (2 k))$ so small that $M 2 k η < δ /3$ , and let $χ$ be the cut-off supplied by Lemma 5.10 for this $η$ . Put $F_{1} := F \cdot χ$ . Then $F_{1}$ is smooth, and its closed support is contained in that of $χ$ , hence in the closed set $R_{k}$ . By part (iii) of Lemma 5.10 applied with $G = F$ , $∥ F - F_{1} ∥_{L^{2} (R_{k})} \leq M 2 k η < δ /3,$ and the triangle inequality gives $∥ F_{0} - F_{1} ∥_{L^{2} (R_{k})} < 2 δ /3 < δ$ . ◻

Proof uses: Lemma 5.10

5.6 Integration formulas on the simplex

The two lemmas below evaluate integrals of monomials over $R_{k} (s)$ . They supply the closed forms used by the certificate pairings of Section 12.

Lemma 5.12 (Dirichlet’s integral over the simplex). For all $k \in N$ and all $a, a_{1}, \dots, a_{k} \in Z_{\geq 0}$ , $\int_{R_{k}} (1 - i = 1 \sum k t_{i})^{a} i = 1 \prod k t_{i}^{a_{i}} d t_{1} \dots d t_{k} = \frac{a ! \prod _{i = 1}^{k} a _{i} !}{( k + a + \sum _{i = 1}^{k} a _{i} ) !} .$

Lean: EuclideanSpace.dirichlet_integral

Uses: Definition 5.1

Proof. One proves the scaled form: for every real $s \geq 0$ , $\int_{R_{k} (s)} (s - i \sum t_{i})^{a} i \prod t_{i}^{a_{i}} d t = s^{k + a + \sum_{i} a_{i}} \frac{a ! \prod _{i} a _{i} !}{( k + a + \sum _{i} a _{i} ) !},$ by induction on $k$ ; the statement of the lemma is the case $s = 1$ . (The scaled form is also what is needed to integrate over $T_{ε}$ and $S_{ε}$ .)

For $k = 0$ both sides equal $s^{a} a! / a! = s^{a}$ . For the inductive step, the integrand is continuous on the compact set $R_{k + 1} (s)$ , hence integrable, and Fubini’s theorem lets us peel off the first coordinate: $\int_{R_{k + 1} (s)} \dots = \int_{0}^{s} t_{1}^{a_{1}} (\int_{R_{k} (s - t_{1})} ((s - t_{1}) - i \geq 2 \sum t_{i})^{a} i \geq 2 \prod t_{i}^{a_{i}} d t_{2} \dots d t_{k + 1}) d t_{1} .$ By the inductive hypothesis applied with scale $s - t_{1}$ , the inner integral equals $(s - t_{1})^{k + a + \sum_{i \geq 2} a_{i}} a! \prod_{i \geq 2} a_{i}! / (k + a + \sum_{i \geq 2} a_{i})!$ . The remaining one-dimensional integral is a Beta integral: for $A, e \in Z_{\geq 0}$ and $s \geq 0$ , $\int_{0}^{s} (s - t)^{A} t^{e} d t = s^{A + e + 1} \frac{A ! e !}{( A + e + 1 )!},$ which follows from $B (A + 1, e + 1) = A! e! / (A + e + 1)!$ after the substitution $t = s u$ . Combining the two factorial expressions and simplifying gives the scaled formula in dimension $k + 1$ . ◻

The lower bound $M_{50, 1/25} > 4$ is established in Section 12 by exact computation with an explicit profile.

Lemma 5.13 (The Beta integral). Let $a, b \geq 1$ be integers. Then $\int_{0}^{1} t^{a - 1} (1 - t)^{b - 1} d t = \frac{( a - 1 )! ( b - 1 )!}{( a + b - 1 )!} .$

Lean: Real.lem_beta_eval

Proof. The integral is the Euler Beta function $B (a, b)$ evaluated at positive integer arguments. For integers it satisfies $B (a, b) = Γ (a) Γ (b) /Γ (a + b)$ , and $Γ (n) = (n - 1)!$ for $n \geq 1$ ; substituting gives the stated quotient of factorials. ◻

6 Auxiliary arithmetic estimates

This section collects the arithmetic estimates used in the sieve analysis: the elementary totient and Möbius identities, the Mertens-type sums over integers coprime to a modulus, the evaluation of the truncated Mertens sum $\sum_{u \leq R, (u, W) = 1} μ (u)^{2} / φ (u)$ , the verification of the sieve-datum hypotheses for the two densities, the asymptotic for the summatory function $H (z)$ of the sieve weight, and the partial-summation lemma that converts $H$ into a $G$ -weighted sum.

Throughout, $W$ , $V$ , $m$ and $M$ denote generic moduli; $W$ and $R$ are the primorial and the truncation of Definitions 3.29 and 3.37, and $e = exp (1)$ denotes the base of the natural logarithm (never a summation variable).

6.1 Elementary totient and Möbius identities

Lemma 6.1 (Multiplicativity formula for $φ$ on a least common multiple). Let $d$ and $e$ be squarefree positive integers (each squarefree; the product $d e$ need not be). Then $φ ([d, e]) φ ((d, e)) = φ (d) φ (e) .$

Lean: PrimeGaps.lem_phi_lcm_product

Uses: Definition 3.4

Proof. Since $d$ and $e$ are squarefree, so are $[d, e]$ and $(d, e)$ , and $φ (n) = p ∣ n \prod (p - 1)$ for every squarefree $n$ . The prime divisors of $[d, e]$ are exactly those of $d$ together with those of $e$ , while the prime divisors of $(d, e)$ are exactly those dividing both. Hence, counting each prime with the multiplicity with which it occurs on either side, $p ∣ [d, e] \prod (p - 1) \cdot p ∣ (d, e) \prod (p - 1) = p ∣ d \prod (p - 1) \cdot p ∣ e \prod (p - 1),$ which is the assertion. ◻

Proof uses: Definition 3.4

Lemma 6.2 (Reciprocal LCM splitting for $φ$ ). Let $d$ and $e$ be squarefree positive integers. Then $\frac{1}{φ ([ d , e ])} = \frac{1}{φ ( d ) φ ( e )} u ∣ (d, e) \sum g (u),$ with $g$ as in Definition 3.6.

Lean: PrimeGaps.lem_lcm_phi_split

Uses: Definition 3.4, Definition 3.6, Lemma 6.1, Lemma 3.10

Proof. By Lemma 6.1, $φ ([d, e]) = φ (d) φ (e) / φ ((d, e))$ , all the factors being positive. The integer $(d, e)$ is squarefree, so Lemma 3.10 applies to it and gives $φ ((d, e)) = \sum_{u ∣ (d, e)} g (u)$ . Substituting and inverting yields the claim. ◻

Proof uses: Lemma 6.1, Lemma 3.10

Lemma 6.3 (Reciprocal LCM splitting). For all positive integers $d, e$ (no squarefreeness required), $\frac{1}{[ d , e ]} = \frac{1}{d e} u ∣ (d, e) \sum φ (u) .$

Lean: PrimeGaps.lem_lcm_split

Uses: Definition 3.4

Proof. The classical identity $\sum_{u ∣ n} φ (u) = n$ , valid for every positive integer $n$ , applied at $n = (d, e)$ turns the right-hand side into $(d, e) / (d e)$ . The claim is then the identity $[d, e] (d, e) = d e$ . ◻

Sublemma 6.4 (Divisor-sum form of $1/ φ$ ). For every squarefree integer $u \geq 1$ , $\frac{1}{φ ( u )} = \frac{1}{u} d ∣ u \sum \frac{μ ( d ) ^{2}}{φ ( d )} .$

Lean: PrimeGaps.one_div_totient_eq_one_div_mul_sum_moebius_sq_div_totient

Uses: Definition 3.4, Definition 3.3

Proof. For squarefree $u$ , $\frac{u}{φ ( u )} = p ∣ u \prod \frac{p}{p - 1} = p ∣ u \prod (1 + \frac{1}{p - 1}) = d ∣ u \sum p ∣ d \prod \frac{1}{p - 1} = d ∣ u \sum \frac{μ ( d ) ^{2}}{φ ( d )} .$ The third equality expands the product over $p ∣ u$ as a sum over the subsets of the prime divisors of $u$ , i.e. over the divisors $d ∣ u$ ; the fourth uses $\prod_{p ∣ d} 1/ (p - 1) = μ (d)^{2} / φ (d)$ on squarefree $d$ . Dividing by $u$ gives the claim. ◻

Sublemma 6.5 (Per-coordinate lcm-decomposition bijection). Let $m$ be a squarefree positive integer, and let $D_{m}$ and $C_{m}$ be the sets $D_{m} C_{m} = = {(d, e) : d, e \geq 1 squarefree, [d, e] = m}, {(c, a, b) : c, a, b \geq 1 pairwise coprime, c ab = m} .$ Then $(d, e) \mapsto ((d, e), d / (d, e), e / (d, e))$ maps $D_{m}$ into $C_{m}$ and is a bijection, with inverse $(c, a, b) \mapsto (c a, c b)$ .

Lean: PrimeGaps.phi_psi_id

Proof. Let $(d, e) \in D_{m}$ and put $c := (d, e)$ , $a := d / c$ , $b := e / c$ . Then $c ab = (d, e) [d, e] / (d, e) \cdot \dots$ ; more directly, $c a = d$ , $c b = e$ and $c ab = d b = d e / (d, e) = [d, e] = m$ . The integers $a$ and $b$ are coprime because any common prime divisor would divide both $d / c$ and $e / c$ and hence, $m$ being squarefree, already lie in $c$ ; the same squarefreeness of $m = c ab$ forces $c$ to be coprime to both $a$ and $b$ . So the map lands in $C_{m}$ .

Conversely let $(c, a, b) \in C_{m}$ and put $d := c a$ , $e := c b$ . Both are divisors of the squarefree $m$ , hence squarefree, and $(d, e) = c$ and $[d, e] = c ab = m$ by pairwise coprimality; so $(d, e) \in D_{m}$ . The two constructions are mutually inverse: starting from $(d, e)$ one recovers $((d, e)) \cdot (d / (d, e)) = d$ and likewise for $e$ ; starting from $(c, a, b)$ one recovers $(c a, c b) \mapsto (c, a, b)$ because $(c a, c b) = c$ when $(a, b) = 1$ . ◻

6.2 Divisor sums, Mertens-type bounds and convergent series

Definition 6.6 (The von Mangoldt function $Λ$ ). Define $Λ : N \to R_{\geq 0}$ by $Λ (n) := {lo g p, 0, n = p^{a} for some prime p and some a \geq 1, otherwise.$

Lemma 6.7 (Mertens’ first theorem, von Mangoldt form). For every integer $N \geq 1$ , $d \leq N \sum \frac{Λ ( d )}{d} - lo g N \leq lo g 4 + 5.$

Uses: Definition 6.6

Proof. Step 1: a Chebyshev upper bound. For every $N \geq 0$ , $d \leq N \sum Λ (d) \leq (lo g 4 + 4) N .$ This is the classical elementary bound obtained from the central binomial coefficient: $\prod_{N < p \leq 2 N} p$ divides $(N 2 N) \leq 4^{N}$ , so $\sum_{N < p \leq 2 N} lo g p \leq N lo g 4$ , and summing the resulting dyadic estimate together with the $O (N lo g N)$ contribution of the proper prime powers gives the stated linear bound with the explicit constant $lo g 4 + 4$ .

Step 2: the factorial identity. Since every $n \geq 1$ satisfies $lo g n = \sum_{d ∣ n} Λ (d)$ , grouping by $d$ gives $n \leq N \sum lo g n = d \leq N \sum Λ (d) ⌊ \frac{N}{d} ⌋ .$ Replacing $⌊ N / d ⌋$ by $N / d$ costs at most $\sum_{d \leq N} Λ (d)$ , which by Step 1 is at most $(lo g 4 + 4) N$ . Hence $n \leq N \sum lo g n - N d \leq N \sum \frac{Λ ( d )}{d} \leq (lo g 4 + 4) N .$

Step 3: Stirling-free evaluation of $\sum_{n \leq N} lo g n$ . Comparing the sum with $\int_{1}^{N} lo g t d t = N lo g N - N + 1$ by monotonicity of $lo g$ gives $\sum_{n \leq N} lo g n - N lo g N \leq N$ . Combining with Step 2 and dividing by $N$ yields $d \leq N \sum \frac{Λ ( d )}{d} - lo g N \leq lo g 4 + 5.$ ◻

Proof uses: Definition 6.6

Lemma 6.8 (Mertens-type estimate for $\sum μ (u)^{2} τ_{k} (u) / φ (u)$ ). For every integer $k \geq 1$ there is a constant $C = C (k) > 0$ such that, for every real $z \geq 2$ , $u \leq z \sum \frac{μ ( u ) ^{2} τ _{k} ( u )}{φ ( u )} \leq C (lo g z)^{k} .$

Lean: ArithmeticFunction.sum_moebius_sq_mul_tau_div_totient_le, WeightedDivisorSum.weightedSum_le

Uses: Definition 3.3, Definition 3.4, Definition 3.5

Proof. Rankin majorisation. For any non-negative $a : N \to R_{\geq 0}$ , any real $Z \geq 1$ and any $κ \geq 0$ one has $(Z / u)^{κ} \geq 1$ for $u \leq Z$ , so $\sum_{u \leq Z} a (u) \leq Z^{κ} \sum_{u \geq 1} a (u) u^{- κ}$ . Apply this with $a (u) := μ (u)^{2} τ_{k} (u) / φ (u)$ and $κ := 1/ lo g (e z) \in (0, 1)$ .

Euler factorisation. The majorant $u \mapsto μ (u)^{2} τ_{k} (u) / (φ (u) u^{κ})$ is non-negative, multiplicative and supported on squarefree integers; since $τ_{k} (p) = k$ and $φ (p) = p - 1$ , and all prime-power terms with exponent $\geq 2$ vanish, $u \geq 1 \sum \frac{μ ( u ) ^{2} τ _{k} ( u )}{φ ( u ) u ^{κ}} = p \prod (1 + \frac{k}{( p - 1 ) p ^{κ}}) .$

Logarithmic bound. Using $lo g (1 + x) \leq x$ and splitting $1/ (p - 1) = 1/ p + 1/ (p (p - 1))$ , $lo g p \prod (1 + \frac{k}{( p - 1 ) p ^{κ}}) \leq k p \sum \frac{1}{p ^{1 + κ}} + k p \sum \frac{1}{p ( p - 1 )},$ and the second sum converges absolutely. For the first, start from Lemma 6.7: discarding the proper prime powers (whose total contribution to $\sum_{d \leq t} Λ (d) / d$ is $O (1)$ , being bounded by $\sum_{p} \sum_{a \geq 2} (lo g p) / p^{a} ≪ \sum_{p} (lo g p) / p^{2}$ ) gives the one-sided prime form $\sum_{p \leq t} (lo g p) / p \leq lo g t + O (1)$ for $t \geq 2$ . Abel summation of this against the weight $1/ lo g t$ yields the elementary one-sided Mertens second bound $\sum_{p \leq t} 1/ p \leq lo g lo g t + B$ with $B$ absolute. A second Abel summation, now against the weight $t^{- κ}$ , gives $\sum_{p} p^{- 1 - κ} = lo g (1/ κ) + O (1)$ . With $κ = 1/ lo g (e z)$ this is $lo g lo g (e z) + O (1) \leq lo g lo g z + O (1)$ for $z \geq 3$ (the range $2 \leq z < 3$ being trivial). Only upper bounds on prime sums are used, so no Tauberian or Dirichlet-series input enters.

Conclusion. Exponentiating gives $\prod_{p} (1 + k (p - 1)^{- 1} p^{- κ}) \leq C_{1} (k) (lo g z)^{k}$ , while $Z^{κ} = z^{1/ l o g (e z)} \leq e$ . Combining with the Rankin majorisation proves the lemma. ◻

Proof uses: Lemma 6.7

Lemma 6.9 (Truncated coprime divisor sum). For every integer $k \geq 1$ there is a constant $C = C (k) > 0$ such that, for every positive integer $D$ and every real $Z \geq 2$ , $r \leq Z (r, D) = 1 \sum \frac{μ ( r ) ^{2} τ _{k} ( r )}{φ ( r )} \leq C (lo g Z)^{k} .$ The constant is independent of $D$ .

Lean: PrimeGaps.lem_truncated_divisor_sum

Uses: Definition 3.3, Definition 3.4, Definition 3.5, Lemma 6.8

Proof. The summand is non-negative, so discarding the coprimality condition only increases the sum; the claim is then Lemma 6.8. (The point of the statement is the uniformity in $D$ : the same constant serves for every modulus, which is what the downstream applications, where $D$ varies with the sieve variables, require.) ◻

Proof uses: Lemma 6.8

Lemma 6.10 ( $k$ -fold restricted reciprocal-totient sum). For every integer $k \geq 1$ there is a constant $C = C (k) > 0$ with the following property. For every real $R \geq 2$ , every modulus $W \geq 1$ and every $d = (d_{1}, \dots, d_{k}) \in Z_{\geq 1}^{k}$ , $(i = 1 \prod k d_{i}) r_{1}, \dots, r_{k} \geq 1 d_{i} ∣ r_{i} \forall i \prod_{i} r_{i} \leq R, μ (\prod_{i} r_{i})^{2} = 1, (\prod_{i} r_{i}, W) = 1 \sum i = 1 \prod k \frac{1}{φ ( r _{i} )} \leq C (lo g R)^{k} .$

Uses: Definition 3.3, Definition 3.4, Lemma 6.8

Proof. Write $r_{i} = d_{i} s_{i}$ and $s^{'} := \prod_{i} s_{i}$ . Because $\prod_{i} r_{i}$ is squarefree, the $d_{i}$ are pairwise coprime and coprime to $s^{'}$ , and $\prod_{i} φ (r_{i}) = φ (\prod_{i} d_{i}) φ (s^{'})$ by multiplicativity of $φ$ on coprime factors. Hence the left-hand side is at most $\frac{\prod _{i} d _{i}}{φ ( \prod _{i} d _{i} )} s^{'} \leq R / \prod_{i} d_{i} μ (s^{'})^{2} = 1, (s^{'}, W \prod_{i} d_{i}) = 1 \sum \frac{τ _{k} ( s ^{'} )}{φ ( s ^{'} )},$ since a squarefree $s^{'}$ arises from at most $τ_{k} (s^{'})$ tuples $(s_{1}, \dots, s_{k})$ with $\prod_{i} s_{i} = s^{'}$ . For the prefactor, the Dirichlet expansion of Lemma 3.12 gives $\prod_{i} d_{i} / φ (\prod_{i} d_{i}) = \sum_{D ∣ \prod_{i} d_{i}} μ (D)^{2} / φ (D)$ , which is bounded by $\sum_{D ∣ \prod_{i} d_{i}} μ (D)^{2} τ_{k} (D) / φ (D)$ ; and every prime dividing $\prod_{i} d_{i}$ is at most $R$ . The remaining $s^{'}$ -sum is a truncated coprime divisor sum at modulus $(W \prod_{i} d_{i})$ , so Lemma 6.9 bounds it by $C (k) (lo g R)^{k}$ with a constant that does not depend on that modulus — the uniformity there is exactly what is needed, since the modulus varies with $d$ . Both factors are thus dominated by the truncated sum $\sum_{u \leq R} μ (u)^{2} τ_{k} (u) / φ (u)$ of Lemma 6.8 — more precisely, the whole expression is bounded by the Euler product $\prod_{p \leq R} (1 + k / (p - 1))$ , and the argument of Lemma 6.8 bounds this by $C (k) (lo g R)^{k}$ for $R \geq 2$ . ◻

Proof uses: Lemma 6.8, Lemma 3.12, Lemma 6.9

Lemma 6.11 (Convergent sum bound for $φ$ ). $s \geq 1 \sum \frac{μ ( s ) ^{2}}{φ ( s ) ^{2}} < \infty.$

Lean: PrimeGaps.lem_convergent_sum_phi

Uses: Definition 3.3, Definition 3.4

Proof. The summand is non-negative, so it suffices to majorise it by a convergent series. The inequality $s \leq φ (s) τ (s)$ established in the proof of Lemma 3.13 gives $1/ φ (s) \leq τ (s) / s$ , whence $\frac{μ ( s ) ^{2}}{φ ( s ) ^{2}} \leq \frac{τ ( s ) ^{2}}{s ^{2}} = \frac{τ ( s )}{s} \cdot \frac{τ ( s )}{s ^{3/2}} \leq \frac{2 τ ( s )}{s ^{3/2}},$ the last step by the elementary bound $τ (s) \leq 2 s$ (divisors pair up as $u \leftrightarrow s / u$ about $s$ ). The Dirichlet series $\sum_{s \geq 1} τ (s) s^{- 3/2} = (\sum_{s \geq 1} s^{- 3/2})^{2}$ converges since $3/2 > 1$ , so the partial sums of the original series are uniformly bounded, and a series of non-negative terms with bounded partial sums converges. ◻

Proof uses: Lemma 3.13

Lemma 6.12 (Convergent sum bound for $g$ ). With $g$ the multiplicative function of Definition 3.6 ( $g (p) = p - 2$ ), $s \geq 1 (s, 2) = 1 \sum \frac{μ ( s ) ^{2}}{g ( s ) ^{2}} < \infty,$ the summand being read as $0$ whenever $μ (s)^{2} = 0$ ; the sum is thus supported on odd squarefree $s$ , for which $g (s) = \prod_{p ∣ s} (p - 2) > 0$ .

Lean: PrimeGaps.convergent_sum_g

Uses: Definition 3.3, Definition 3.6

Proof. The summand is non-negative and multiplicative, supported on odd squarefree integers. Its local factor at an odd prime $p$ is $1 + (p - 2)^{- 2}$ , and at $p = 2$ it is $1$ . Since $(p - 2)^{- 2} \leq 9 p^{- 2}$ for every odd prime $p$ (indeed $p - 2 \geq p /3$ for $p \geq 3$ ), the series $\sum_{p} (p - 2)^{- 2}$ converges, so $\prod_{p odd} (1 + (p - 2)^{- 2}) < \infty$ . Every partial sum over a finite set of integers is bounded by this Euler product, whence convergence. ◻

6.3 The constants $A (M)$ and $B (M)$

Sublemma 6.13 (Euler product for $ζ (2)$ ). With $ζ (2) = \sum_{n \geq 1} n^{- 2}$ , $ζ (2) = p \prod (1 - \frac{1}{p ^{2}})^{- 1},$ both the series and the product being convergent.

Lean: PrimeGaps.eulerProduct_zetaTwo, PrimeGaps.multipliable_eulerProduct_zetaTwo, PrimeGaps.summable_zetaTwo

Proof. By unique factorisation, every $n \geq 1$ has a unique representation $n = \prod_{p} p^{a_{p}}$ with $a_{p} \geq 0$ and only finitely many $a_{p}$ non-zero, so $n^{- 2} = \prod_{p} p^{- 2 a_{p}}$ . The series $\sum_{n} n^{- 2}$ converges absolutely (it is bounded by $1 + \int_{1}^{\infty} t^{- 2} d t = 2$ ), which licenses reorganising it as a product over primes of the geometric series $\sum_{a \geq 0} p^{- 2 a} = (1 - p^{- 2})^{- 1}$ ; the rearrangement is justified by letting $P \to \infty$ in the partial product over $p \leq P$ , whose expansion exhausts all $n \geq 1$ in the limit. ◻

Definition 6.14 (The auxiliary Dirichlet sum $A (M)$ ). For every positive integer $M$ , set $A (M) := e \geq 1 (e, M) = 1 \sum \frac{μ ( e )}{e ^{2}} .$

Lean: PrimeGaps.A

Uses: Definition 3.3

Sublemma 6.15 (Absolute convergence and the bound $∣ A (M) ∣ \leq ζ (2)$ ). For every positive integer $M$ the series of Definition 6.14 converges absolutely, and $∣ A (M) ∣ \leq ζ (2)$ .

Lean: PrimeGaps.A_abs_le_zetaTwo

Uses: Definition 6.14

Proof. Each summand satisfies $∣ μ (e) / e^{2} ∣ \leq 1/ e^{2}$ , so $e \geq 1 (e, M) = 1 \sum \frac{μ ( e )}{e ^{2}} \leq e \geq 1 \sum \frac{1}{e ^{2}} = ζ (2) < \infty.$ This is absolute convergence, and the triangle inequality applied to the (absolutely convergent) sum gives $∣ A (M) ∣ \leq ζ (2)$ . ◻

Sublemma 6.16 (Closed form for $A (M)$ in terms of $ζ (2)$ ). For every positive integer $M$ (squarefreeness is not required), $A (M) = \frac{1/ ζ ( 2 )}{\prod _{p ∣ M} ( 1 - 1/ p ^{2} )} .$

Lean: PrimeGaps.A_closed_form

Uses: Definition 6.14, Sublemma 6.13, Sublemma 6.15

Proof. By Sublemma 6.15 the defining series converges absolutely, so it may be expanded as an Euler product. Its local factor at a prime $p ∣ M$ is $1$ (only $e = 1$ contributes at that prime), and at a prime $p ∤ M$ it is $\sum_{a \geq 0} μ (p^{a}) p^{- 2 a} = 1 - p^{- 2}$ , since $μ (p^{a}) = 0$ for $a \geq 2$ . Hence $A (M) = p ∤ M \prod (1 - \frac{1}{p ^{2}}) .$ Splitting the product over all primes as $\prod_{p} = \prod_{p ∣ M} \cdot \prod_{p ∤ M}$ and invoking $\prod_{p} (1 - p^{- 2}) = 1/ ζ (2)$ (Sublemma 6.13) gives the stated closed form. Note that only the set of prime divisors of $M$ enters, which is why no squarefreeness hypothesis is needed. ◻

Proof uses: Sublemma 6.13, Sublemma 6.15

Definition 6.17 (The auxiliary Dirichlet sum $B (M)$ ). For every positive integer $M$ , set $B (M) := e \geq 1 (e, M) = 1 \sum \frac{μ ( e ) lo g e}{e ^{2}} .$ The series converges absolutely, since $∣ μ (e) lo g e / e^{2} ∣ \leq (lo g e) / e^{2}$ and $\sum_{e \geq 1} (lo g e) / e^{2} < \infty$ .

Lean: PrimeGaps.B

Uses: Definition 3.3

6.4 Coprime harmonic and coprime-density sums

Definition 6.18 (The prime-cost quantity $ℓ_{m}$ ). For a positive integer $m$ , set $ℓ_{m} := p ∣ m \sum \frac{lo g p}{p - 1},$ the sum running over the distinct prime divisors of $m$ .

Lean: PrimeGaps.ellV

Sublemma 6.19 (Coprime harmonic sum). There is an absolute constant $C > 0$ such that, for every squarefree integer $m \geq 1$ and every real $Z \geq 1$ , $n \leq Z (n, m) = 1 \sum \frac{1}{n} - \frac{φ ( m )}{m} (lo g Z + γ_{0} + ℓ_{m}) \leq C \frac{τ ( m )}{Z},$ where $γ_{0}$ is the Euler–Mascheroni constant.

Lean: PrimeGaps.coprime_reciprocal_sum_asymptotic

Uses: Definition 6.18, Definition 3.3, Definition 3.4

Proof. Detect the coprimality condition by $1 [(n, m) = 1] = \sum_{d ∣ (n, m)} μ (d)$ and swap the two finite sums: $n \leq Z (n, m) = 1 \sum \frac{1}{n} = d ∣ m \sum μ (d) n \leq Z d ∣ n \sum \frac{1}{n} = d ∣ m \sum \frac{μ ( d )}{d} n^{'} \leq Z / d \sum \frac{1}{n ^{'}} .$ The classical harmonic estimate $\sum_{n^{'} \leq Y} 1/ n^{'} = lo g Y + γ_{0} + O (1/ Y)$ gives $n \leq Z (n, m) = 1 \sum \frac{1}{n} = (lo g Z + γ_{0}) d ∣ m \sum \frac{μ ( d )}{d} - d ∣ m \sum \frac{μ ( d ) lo g d}{d} + O (\frac{τ ( m )}{Z}),$ the error using $\sum_{d ∣ m} ∣ μ (d) ∣ = τ (m)$ for squarefree $m$ . Now $\sum_{d ∣ m} μ (d) / d = \prod_{p ∣ m} (1 - 1/ p) = φ (m) / m$ , and differentiating the identity $\sum_{d ∣ m} μ (d) d^{- s} = \prod_{p ∣ m} (1 - p^{- s})$ at $s = 1$ gives $- d ∣ m \sum \frac{μ ( d ) lo g d}{d} = p ∣ m \prod (1 - \frac{1}{p}) p ∣ m \sum \frac{p ^{- 1} lo g p}{1 - p ^{- 1}} = \frac{φ ( m )}{m} ℓ_{m} .$ Combining the three displays proves the claim, with an absolute implied constant. ◻

Lemma 6.20 (Mertens sum $\sum 1/ n$ restricted to $(n, W) = 1$ ). There is an absolute constant $C > 0$ with the following property. Let $W \geq 1$ be a squarefree integer and let $x$ be a real number with $x \geq \frac{W τ ( W )}{φ ( W )} .$ Then $n \leq x (n, W) = 1 \sum \frac{1}{n} - \frac{φ ( W )}{W} lo g x \leq C \frac{φ ( W )}{W} (1 + lo g lo g (e W)) .$

Lean: PrimeGaps.mertens_reciprocal_general

Uses: Definition 3.3, Definition 3.4, Sublemma 6.19, Definition 6.18

Proof. Sublemma 6.19 applied with $m = W$ and $Z = x$ gives $n \leq x (n, W) = 1 \sum \frac{1}{n} = \frac{φ ( W )}{W} (lo g x + γ_{0} + ℓ_{W}) + O (\frac{τ ( W )}{x}) .$ The hypothesis on $x$ is exactly $τ (W) / x \leq φ (W) / W$ , so the error term is $O (φ (W) / W)$ ; the same bound covers the constant $γ_{0} φ (W) / W$ . It remains to bound $ℓ_{W} = \sum_{p ∣ W} (lo g p) / (p - 1)$ . Split the prime divisors of $W$ at $1 + lo g W$ . For $p > 1 + lo g W$ , use $\sum_{p ∣ W} lo g p = lo g W$ (valid since $W$ is squarefree) and $p - 1 > lo g W$ to bound that part by $1$ ; more crudely, the contribution is $O (1)$ . For $p \leq 1 + lo g W$ , use $(lo g p) / (p - 1) \leq 2 (lo g p) / p$ and the elementary Mertens bound $\sum_{p \leq t} (lo g p) / p \leq lo g t + O (1)$ of Lemma 6.7 with $t = 1 + lo g W$ , which gives $O (lo g (1 + lo g W)) = O (1 + lo g lo g (e W))$ . Hence $ℓ_{W} ≪ 1 + lo g lo g (e W)$ , and collecting all error contributions proves the lemma. The normalisation $1 + lo g lo g (e W)$ rather than $lo g lo g W$ is used so that the error term is defined and non-negative for every $W \geq 1$ ; for large $W$ the two agree up to an additive constant. ◻

Proof uses: Sublemma 6.19, Definition 6.18, Lemma 6.7

Definition 6.21 (The coprime density partial sum $A_{m} (x)$ ). For a positive integer $m$ and a real number $x$ , set $A_{m} (x) := f \leq x (f, m) = 1 \sum \frac{μ ( f ) ^{2}}{φ ( f )},$ the sum running over the positive integers $f \leq x$ coprime to $m$ ; thus $A_{m} (x) = 0$ for $x < 1$ .

Lean: PrimeGaps.MaynardOffDiagonal.sumA

Uses: Definition 3.3, Definition 3.4

Sublemma 6.22 (Coprime density sum). There is an absolute constant $C > 0$ such that, for every squarefree integer $m \geq 1$ and every real $x \geq 2$ , $A_{m} (x) - \frac{φ ( m )}{m} (lo g x + ℓ_{m}) \leq C (\frac{φ ( m )}{m} + \frac{τ ( m ) lo g ( 2 m x )}{x}) .$

Lean: PrimeGaps.exists_abs_sumA_sub_le

Uses: Definition 6.21, Definition 6.18, Sublemma 6.19

Proof. Step 1: a Dirichlet cofactor. Let $κ$ be the multiplicative function defined by the Dirichlet convolution identity $μ^{2} / φ = κ * (1/ id)$ , i.e. $\frac{μ ( f ) ^{2}}{φ ( f )} = d e = f \sum κ (d) \frac{1}{e} .$ Comparing local Euler factors shows $κ (1) = 1$ , $κ (p) = 1/ (p (p - 1))$ , $κ (p^{2}) = - 1/ (p (p - 1))$ and $κ (p^{j}) = 0$ for $j \geq 3$ ; in particular $κ$ is supported on cube-free integers, its local factor $1 + κ (p) + κ (p^{2})$ equals $1$ at every prime, and $d \geq 1 \sum ∣ κ (d) ∣ d d \geq 1 \sum ∣ κ (d) ∣ lo g (2 d) < < \infty, \infty.$ Both convergence statements follow from the Euler-product bound $\sum_{j \geq 0} ∣ κ (p^{j}) ∣ p^{j /2} \leq exp (2 p^{- 3/2})$ , together with the elementary partial-summation bound $\sum_{d \leq X} ∣ κ (d) ∣ d ≪ X lo g (2 X)$ , which in turn comes from writing a cube-free $d$ uniquely as $b^{2} a$ with $a$ squarefree, $(a, b) = 1$ , and using $\sum_{b \leq X} 1/ φ (b) ≪ 1 + lo g X$ . Consequently, for every $Y \geq 1$ , $d \geq Y \sum ∣ κ (d) ∣ d \geq Y \sum ∣ κ (d) ∣ lo g (d / Y) ≪ ≪ \frac{lo g ( 2 Y )}{Y}, \frac{lo g ( 2 Y )}{Y}$ (a dyadic decomposition of the range $d \geq Y$ ).

Step 2: the hyperbola identity. Summing $μ^{2} / φ = κ * (1/ id)$ over $f \leq x$ with $(f, m) = 1$ and noting that $(f, m) = 1$ is equivalent to $(d, m) = (e, m) = 1$ for $f = d e$ , $A_{m} (x) = d \leq x (d, m) = 1 \sum κ (d) e \leq x / d (e, m) = 1 \sum \frac{1}{e} .$

Step 3: insert the harmonic asymptotic. Apply Sublemma 6.19 to the inner sum for each $d$ , obtaining the main term $\frac{φ ( m )}{m} (lo g (x / d) + γ_{0} + ℓ_{m})$ and an error $O (τ (m) d / x)$ ; the errors sum, against $\sum_{d \leq x} ∣ κ (d) ∣ d ≪ x lo g (2 x)$ , to $O (τ (m) lo g (2 x) / x)$ . For the main term, complete the $d$ -sum to all $d \geq 1$ coprime to $m$ ; by Step 1 the discarded tail $d > x$ contributes $O (τ (m) lo g (2 m x) / x)$ (using $ℓ_{m} \leq lo g m$ to absorb the $m$ into the logarithm). Since $κ$ has local mass $1$ at every prime, $\sum_{(d, m) = 1} κ (d) = 1$ , and the completed main term is $\frac{φ ( m )}{m} (lo g x + γ_{0} + ℓ_{m}) - \frac{φ ( m )}{m} d \geq 1 (d, m) = 1 \sum κ (d) lo g d .$ The last sum is $O (1)$ by the second convergence statement of Step 1, and $γ_{0} φ (m) / m = O (φ (m) / m)$ . Collecting all contributions gives the stated bound, with an absolute constant. ◻

Proof uses: Sublemma 6.19, Definition 6.18, Definition 6.21

6.5 The sum $T_{d}$ and the Mertens sum over integers coprime to $W$

Definition 6.23 (The auxiliary sum $T_{d}$ ). Let $R \geq 1$ be real and let $W \geq 1$ and $d \geq 1$ be integers. Set $T_{d} := v \leq R / d (v, d W) = 1 \sum \frac{μ ( v ) ^{2}}{v} .$ The sum is empty, and hence $T_{d} = 0$ , once $d > R$ .

Lean: PrimeGaps.TInner

Uses: Definition 3.3

Sublemma 6.24 (Outer-sum decomposition for $\sum μ^{2} / φ$ ). For every integer $R \geq 1$ and every integer $W \geq 1$ , $u \leq R (u, W) = 1 \sum \frac{μ ( u ) ^{2}}{φ ( u )} = d \leq R (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{d φ ( d )} T_{d},$ with $T_{d}$ as in Definition 6.23.

Lean: PrimeGaps.sum_moebius_sq_div_totient_eq_sum_mul_TInner

Uses: Definition 6.23, Definition 3.3, Definition 3.4

Proof. Substitute the identity $1/ φ (u) = (1/ u) \sum_{d ∣ u} μ (d)^{2} / φ (d)$ of Sublemma 6.4 — legitimate because $μ (u)^{2} \neq = 0$ restricts the outer sum to squarefree $u$ — and swap the two finite summations: $u \leq R (u, W) = 1 \sum \frac{μ ( u ) ^{2}}{φ ( u )} = d \leq R (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{φ ( d )} u \leq R, d ∣ u (u, W) = 1 \sum \frac{μ ( u ) ^{2}}{u} .$ Fix a squarefree $d$ with $(d, W) = 1$ and write $u = d v$ with $v \leq R / d$ . On the support of $μ (u)^{2}$ the integer $u$ is squarefree, which for $u = d v$ is equivalent to $v$ squarefree with $(v, d) = 1$ ; and $(u, W) = 1$ together with $(d, W) = 1$ is equivalent to $(v, W) = 1$ . So the conditions on $u$ become “ $v$ squarefree and $(v, d W) = 1$ ”. Since $μ (u)^{2} / u = μ (v)^{2} / (d v)$ on that support, the inner sum equals $T_{d} / d$ , which is the claim. ◻

Proof uses: Sublemma 6.4

Sublemma 6.25 (Möbius squarefree-inversion step for $T_{d}$ ). For every real $R \geq 1$ , every integer $W \geq 1$ and every integer $d \geq 1$ (no squarefreeness or coprimality is required), $T_{d} = e \leq R / d (e, d W) = 1 \sum \frac{μ ( e )}{e ^{2}} w \leq R / (d e^{2}) (w, d W) = 1 \sum \frac{1}{w} .$

Lean: PrimeGaps.T_decomposition

Uses: Definition 6.23, Definition 3.3

Proof. Start from the squarefree-detection identity $μ (v)^{2} = \sum_{e^{2} ∣ v} μ (e)$ , valid for every positive integer $v$ : both sides are multiplicative, and at a prime power $p^{a}$ the right-hand side is $1$ for $a \in {0, 1}$ and $1 + μ (p) = 0$ for $a \geq 2$ , matching $μ (p^{a})^{2}$ . Insert it into $T_{d} = \sum_{v \leq R / d, (v, d W) = 1} μ (v)^{2} / v$ and swap the two finite sums. Writing $v = e^{2} w$ turns the constraint $e^{2} ∣ v$ into a free $w$ -sum with $w \leq R / (d e^{2})$ , and the constraint $(v, d W) = 1$ into $(e, d W) = (w, d W) = 1$ ; the $e$ -range is $e \leq R / d$ because $e^{2} \leq v \leq R / d$ . Since $1/ v = (1/ e^{2}) (1/ w)$ , the displayed identity follows. (When $(e, d W) > 1$ the inner sum is empty, so restricting the $e$ -sum to $(e, d W) = 1$ changes nothing.) ◻

Sublemma 6.26 (Inner $w$ -sum via Mertens for $e \leq R^{1/8}$ ). There is a constant $C > 0$ such that, for all sufficiently large $N$ , the following holds for every squarefree $d$ with $(d, W) = 1$ and $d \leq R^{1/2}$ and every integer $e$ with $1 \leq e \leq R^{1/8}$ and $(e, d W) = 1$ . Let $W = d W$ . Then $w \leq R / (d e^{2}) (w, W) = 1 \sum \frac{1}{w} - \frac{φ ( W )}{W} (lo g R - lo g d - 2 lo g e) \leq C \frac{φ ( W )}{W} (1 + lo g lo g (e W)) .$

Lean: PrimeGaps.slem_T_d_inner_w_sum

Uses: Definition 3.37, Definition 3.29, Lemma 6.20, Lemma 3.32

Proof. Since $d$ is squarefree, $W$ is squarefree (Definition 3.29) and $(d, W) = 1$ , the modulus $W = d W$ is a positive squarefree integer. We apply Lemma 6.20 with this modulus and with $x := R / (d e^{2})$ , and must verify $x \geq W τ (W) / φ (W)$ .

Lower bound on $x$ . From $d \leq R^{1/2}$ and $e \leq R^{1/8}$ we get $d e^{2} \leq R^{1/2} \cdot R^{1/4} = R^{3/4}$ , hence $x = R / (d e^{2}) \geq R^{1/4}$ .

Upper bound on $W τ (W) / φ (W)$ . For squarefree $n$ the quantity $n τ (n) / φ (n)$ factors over the primes dividing $n$ , each contributing $2 p / (p - 1) \leq 4$ ; hence $W τ (W) / φ (W) \leq 4^{ω (W)}$ . Next, for any fixed integer $B \geq 2$ , splitting the prime divisors of $n$ at $B$ gives $ω (n) \leq π (B) + lo g n / lo g B$ , hence $4^{ω (n)} \leq 4^{π (B)} n^{l o g 4/ l o g B}$ . Choose $B := 4^{8} = 65536$ , so that $lo g 4/ lo g B = 1/8$ and, with $K := 4^{π (B)}$ an absolute constant, $\frac{W τ ( W )}{φ ( W )} \leq K W^{1/8} .$ By Lemma 3.32 we have $W ≪ (lo g lo g N)^{2}$ , and $d \leq R^{1/2}$ , so $W = d W \leq R^{1/2} (lo g lo g N)^{2}$ and therefore $\frac{W τ ( W )}{φ ( W )} \leq K R^{1/16} (lo g lo g N)^{1/4} .$ Since $R = N^{ϑ /2 - δ}$ is a fixed positive power of $N$ , the right-hand side is $\leq R^{1/4} \leq x$ for all sufficiently large $N$ , the factor $(lo g lo g N)^{1/4}$ being of lower order than $R^{3/16}$ . This verifies the hypothesis.

With the hypothesis verified, Lemma 6.20 gives $w \leq R / (d e^{2}) (w, W) = 1 \sum \frac{1}{w} - \frac{φ ( W )}{W} lo g \frac{R}{d e ^{2}} \leq C \frac{φ ( W )}{W} (1 + lo g lo g (e W)),$ and $lo g (R / (d e^{2})) = lo g R - lo g d - 2 lo g e$ . ◻

Proof uses: Lemma 6.20, Lemma 3.32

Sublemma 6.27 (Evaluation of $T_{d}$ ). There is a constant $C > 0$ such that, for all sufficiently large $N$ and every squarefree $d$ with $(d, W) = 1$ and $d \leq R^{1/2}$ . Let $W = d W$ . Then $T_{d} - \frac{φ ( W )}{W} [A (W) lo g (R / d) - 2 B (W)] \leq C \frac{φ ( W )}{W} (lo g (2 d) + lo g lo g W) + C \frac{lo g R}{R ^{1/8}} .$

Lean: PrimeGaps.slem_T_d_eval

Uses: Definition 6.23, Definition 3.37, Definition 3.29, Definition 6.14, Definition 6.17

Proof. Sublemma 6.25 rewrites $T_{d}$ as an $e$ -sum weighted by $μ (e) / e^{2}$ times an inner $w$ -sum. Split the $e$ -range at $e = R^{1/8}$ .

Range $e \leq R^{1/8}$ . Sublemma 6.26 evaluates the inner sum for each such $e$ , with error $O (\frac{φ ( W )}{W} (1 + lo g lo g (e W)))$ . Summing the main term against $μ (e) / e^{2}$ over $e \leq R^{1/8}$ coprime to $W$ produces $\frac{φ ( W )}{W} [lo g (R / d) e \leq R^{1/8} (e, W) = 1 \sum \frac{μ ( e )}{e ^{2}} - 2 e \leq R^{1/8} (e, W) = 1 \sum \frac{μ ( e ) lo g e}{e ^{2}}] .$ Completing both $e$ -sums to infinity replaces them by $A (W)$ and $B (W)$ of Definitions 6.14 and 6.17; by the tail bounds $A (M) - \sum_{e \leq m} \leq 1/ m$ and $B (M) - \sum_{e \leq m} \leq (lo g m + 1) / m$ (each a comparison with $\sum_{e > m} e^{- 2}$ and $\sum_{e > m} (lo g e) e^{- 2}$ respectively), applied at $m = ⌊ R^{1/8} ⌋$ , the cost is $O (lo g R \cdot R^{- 1/8})$ . The accumulated error terms contribute $O (\frac{φ ( W )}{W} (1 + lo g lo g (e W)))$ after summation against $\sum_{e} e^{- 2} \leq 2$ .

Range $e > R^{1/8}$ . Here use the trivial bounds $∣ μ (e) / e^{2} ∣ \leq 1/ e^{2}$ and $\sum_{w \leq R / (d e^{2})} 1/ w \leq 1 + lo g R$ , so this part is $≪ lo g R e > R^{1/8} \sum \frac{1}{e ^{2}} ≪ \frac{lo g R}{R ^{1/8}} .$

Normalising the error. Finally $lo g lo g (e W) = lo g lo g (e d W) ≪ lo g (2 d) + lo g lo g W$ for $W \geq e$ , which converts the middle error into the stated shape. Adding the three contributions gives the sublemma. ◻

Proof uses: Sublemma 6.25, Sublemma 6.26, Definition 6.14, Definition 6.17

Sublemma 6.28 (Tail bound for $d > R^{1/2}$ ). There is a constant $C > 0$ such that, for all sufficiently large $N$ , $d > R, d squarefree (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{d φ ( d )} T_{d} \leq C \frac{( lo g R ) ^{3}}{R} .$

Lean: PrimeGaps.tailSum_ll

Uses: Definition 6.23, Definition 3.37, Definition 3.29

Proof. From $μ (v)^{2} / v \leq 1/ v$ and $\sum_{v \leq R / d} 1/ v \leq 1 + lo g R$ we get $0 \leq T_{d} \leq 1 + lo g R ≪ lo g R$ for $R \geq 2$ , uniformly in $d$ and $W$ . By Lemma 3.13, $1/ (d φ (d)) \leq τ (d) / d^{2}$ . Lemma 6.8 with $k = 2$ gives $\sum_{d \leq X} μ (d)^{2} τ (d) / φ (d) ≪ (lo g X)^{2}$ , hence also $\sum_{d \leq X} μ (d)^{2} τ (d) / d ≪ (lo g X)^{2}$ ; partial summation converts this into the tail estimate $d > Y \sum \frac{μ ( d ) ^{2} τ ( d )}{d ^{2}} ≪ \frac{( lo g Y ) ^{2} + 1}{Y} .$ Applying it with $Y = R$ bounds $\sum_{d > R} μ (d)^{2} / (d φ (d)) ≪ (lo g R)^{2} / R$ , and multiplying by the uniform bound $T_{d} ≪ lo g R$ gives the claim. ◻

Proof uses: Lemma 3.13, Lemma 6.8

Sublemma 6.29 (Leading-coefficient telescoping identity). For every integer $W \geq 1$ , $d \geq 1 (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{d ^{2}} A (d W) = 1.$

Lean: PrimeGaps.main_thm

Uses: Definition 6.14, Sublemma 6.16, Sublemma 6.13, Sublemma 6.15

Proof. Write $f (d) := μ (d)^{2} A (d W) / d^{2}$ . By Sublemma 6.16, $A (d W) = (1/ ζ (2)) / \prod_{p ∣ d W} (1 - p^{- 2})$ , so for squarefree $d$ coprime to $W$ $f (d) = A (W) p ∣ d \prod \frac{1/ p ^{2}}{1 - 1/ p ^{2}} .$ In particular $f (1) = A (W)$ , and $f$ is multiplicative up to the normalising constant $A (W)$ : for coprime squarefree $d_{1}, d_{2}$ both coprime to $W$ one has $f (d_{1} d_{2}) A (W) = f (d_{1}) f (d_{2})$ ; and at a prime $p ∤ W$ , $f (p) = p^{- 2} A (W) / (1 - p^{- 2})$ . Since the values of $f$ at distinct primes multiply in this normalised sense, and $μ (d)^{2}$ restricts the sum to squarefree $d$ , each prime $p ∤ W$ contributes independently either $1$ or $p^{- 2} (1 - p^{- 2})^{- 1}$ , giving $d \geq 1 (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{d ^{2}} A (d W) = A (W) p ∤ W \prod (1 + \frac{1}{p ^{2}} \cdot \frac{1}{1 - 1/ p ^{2}}) .$ (The rearrangement is licensed by absolute convergence: $∣ A (d W) ∣ \leq ζ (2)$ by Sublemma 6.15 and $\sum_{d} d^{- 2} < \infty$ .) The elementary identity $1 + x / (1 - x) = 1/ (1 - x)$ with $x = p^{- 2}$ turns the local factor into $(1 - p^{- 2})^{- 1}$ , so the product equals $\prod_{p ∤ W} (1 - p^{- 2})^{- 1}$ . Combining with $A (W) = (1/ ζ (2)) / \prod_{p ∣ W} (1 - p^{- 2})$ , $d \geq 1 (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{d ^{2}} A (d W) = \frac{1/ ζ ( 2 )}{\prod _{p ∣ W} ( 1 - p ^{- 2} ) \prod _{p ∤ W} ( 1 - p ^{- 2} )} = \frac{1/ ζ ( 2 )}{\prod _{p} ( 1 - p ^{- 2} )} = 1,$ the last equality by Sublemma 6.13. ◻

Proof uses: Sublemma 6.16, Sublemma 6.15, Sublemma 6.13

Lemma 6.30 (Mertens sum over $u$ coprime to $W$ ). Let $R$ and $W$ be as in Definitions 3.37 and 3.29. There is a constant $C > 0$ such that, for all sufficiently large $N$ , $u \leq R (u, W) = 1 \sum \frac{μ ( u ) ^{2}}{φ ( u )} - \frac{φ ( W )}{W} lo g R \leq C \frac{φ ( W )}{W} lo g lo g W .$

Lean: PrimeGaps.lem_mertens_W

Uses: Definition 3.37, Definition 3.29, Definition 3.3, Definition 3.4

Proof. By Sublemma 6.24 the left-hand sum equals $\sum_{d} μ (d)^{2} T_{d} / (d φ (d))$ . Sublemma 6.28 bounds the contribution of $d > R$ by $O ((lo g R)^{3} / R)$ , which is $o (φ (W) / W)$ for large $N$ since $φ (W) / W ≫ 1/ lo g lo g N$ by Lemma 3.32. Restrict to $d \leq R$ .

Insert the expansion of Sublemma 6.27 and use $φ (d W) / (d W) = (φ (d) / d) (φ (W) / W)$ , valid because $(d, W) = 1$ . This gives $u \leq R (u, W) = 1 \sum \frac{μ ( u ) ^{2}}{φ ( u )} = \frac{φ ( W )}{W} [(lo g R) S_{1} - S_{2} - 2 S_{3}] + O (\frac{φ ( W )}{W} lo g lo g W),$ where, with all sums over squarefree $d$ coprime to $W$ , $S_{1} S_{2} S_{3} := := := d \sum \frac{μ ( d ) ^{2} A ( d W )}{d ^{2}}, d \sum \frac{μ ( d ) ^{2} ( lo g d ) A ( d W )}{d ^{2}}, d \sum \frac{μ ( d ) ^{2} B ( d W )}{d ^{2}},$ and the error term also absorbs the $lo g (2 d)$ contributions of Sublemma 6.27 (which sum, against $μ (d)^{2} φ (d) / (d^{2} φ (d)) \leq d^{- 2}$ , to $O (1)$ ) and the $O (lo g R / R^{1/8})$ terms. By Sublemma 6.29, $S_{1} = 1$ once the $d$ -sum is completed, and completing it costs $O (R^{- 1/2})$ by Sublemma 6.15. The sums $S_{2}$ and $S_{3}$ are $O (1)$ in absolute value: each is bounded by $ζ (2) \sum_{d \geq 1} (1 + lo g d) / d^{2} ≪ 1$ , again using $∣ A (M) ∣, ∣ B (M) ∣ ≪ 1$ from Sublemma 6.15 and the corresponding trivial bound for $B$ . Assembling and absorbing the $O (1)$ and $O (R^{- 1/2} lo g R)$ contributions into $O (\frac{φ ( W )}{W} lo g lo g W)$ — legitimate since $lo g lo g W \geq 1$ for $N$ large — gives the lemma. ◻

Proof uses: Sublemma 6.24, Sublemma 6.28, Sublemma 6.27, Sublemma 6.29, Sublemma 6.15, Lemma 3.32, Definition 6.14, Definition 6.17

6.6 The two sieve densities

Throughout this subsection $(γ, V)$ denotes a sieve datum in the sense of Definition 4.3, with parameters $A_{1}, A_{2}, A_{3}, L$ , and $g_{*}$ is the derived totally multiplicative function of Definition 4.4. We write $Δ (γ; w, z) := w \leq p \leq z \sum \frac{γ ( p ) lo g p}{p} - lo g (z / w) (2 \leq w \leq z)$ for the Mertens deviation of a density $γ$ .

Sublemma 6.31 ( $g_{*}$ for the Maynard datum). For the Maynard sieve datum (Definition 4.29) and every squarefree $r \geq 1$ , $g_{*} (r) = ⎩ ⎨ ⎧ \frac{μ ( r ) ^{2}}{g ( r )}, 0, (r, W) = 1, (r, W) > 1,$ with $g$ the multiplicative function of Definition 3.6.

Lean: PrimeGaps.maynardSieveDatum_gStar_not_coprime, PrimeGaps.maynardSieveDatum_gStar_squarefree_coprime

Uses: Definition 4.29, Definition 4.4, Definition 3.6, Definition 3.29

Proof. Both sides are totally multiplicative in $r$ , so it suffices to compare them at primes. If $p ∣ W$ then $γ_{g} (p) = 0$ , so $g_{*} (p) = 0$ ; total multiplicativity then forces $g_{*} (r) = 0$ whenever some prime divisor of $r$ divides $W$ , i.e. whenever $(r, W) > 1$ . If $p ∤ W$ then $γ_{g} (p) = p / (p - 1)$ and $g_{*} (p) = \frac{γ _{g} ( p )}{p - γ _{g} ( p )} = \frac{p / ( p - 1 )}{p - p / ( p - 1 )} = \frac{1}{p - 2} = \frac{1}{g ( p )} .$ For squarefree $r$ coprime to $W$ we have $μ (r)^{2} = 1$ , and multiplying the prime-level identities over the (distinct) primes dividing $r$ gives $g_{*} (r) = 1/ g (r)$ . ◻

Proof uses: Lemma 4.5

A family of densities $(γ_{N})_{N \geq 1}$ is called $W$ -tricked if each $γ_{N}$ is multiplicative and non-negative with $γ_{N} (1) = 1$ , if $γ_{N} (p) = 0$ for every prime $p ∣ W$ , and if there is a single constant $c > 0$ , independent of $N$ , with $∣ γ_{N} (p) - 1∣ \leq c / p$ for every prime $p ∤ W$ . Both $γ_{g}$ and $γ^{(m)}$ are $W$ -tricked, with $c$ absolute. The next two sublemmas supply the two Mertens-deviation constants that a sieve datum (Definition 4.3) requires.

Sublemma 6.32 (Singular product for $γ_{g}$ ). There are constants $C > 0$ and $N_{0}$ such that, for every $N \geq N_{0}$ with $D_{0} \geq 2$ , $S (γ_{g}) - \frac{φ ( W )}{W} \leq C \frac{φ ( W )}{W} \cdot \frac{1}{D _{0}},$ with $S$ as in Notation 3.41. Equivalently, $S (γ_{g}) = \frac{φ ( W )}{W} (1 + O (1/ D_{0}))$ .

Lean: PrimeGaps.singularSeries_maynardSieveDatum_γ_asymptotic

Uses: Notation 3.41, Definition 4.29, Definition 3.29, Definition 3.28

Proof. Split the defining product $S (γ_{g}) = \prod_{p} (1 - γ_{g} (p) / p)^{- 1} (1 - 1/ p)$ over $p ∣ W$ and $p ∤ W$ . For $p ∣ W$ one has $γ_{g} (p) = 0$ and the local factor is $1 - 1/ p$ ; the product of these over $p ∣ W$ is $φ (W) / W$ . For $p ∤ W$ one has $γ_{g} (p) = p / (p - 1)$ , so $(1 - \frac{γ _{g} ( p )}{p})^{- 1} (1 - \frac{1}{p}) = (1 - \frac{1}{p - 1})^{- 1} \frac{p - 1}{p} = \frac{( p - 1 ) ^{2}}{p ( p - 2 )} = 1 + \frac{1}{p ( p - 2 )} .$ Every such $p$ exceeds $D_{0}$ , so the tail product satisfies $1 \leq \prod_{p > D_{0}} (1 + \frac{1}{p ( p - 2 )}) \leq exp (\sum_{p > D_{0}} \frac{1}{p ( p - 2 )}) \leq exp (2/ D_{0})$ , using $\sum_{n > t} n^{- 2} \leq 2/ t$ and $p (p - 2) \geq p^{2} /3$ for $p \geq 3$ . Since $e^{2/ D_{0}} - 1 \leq 4/ D_{0}$ for $D_{0} \geq 4$ , the tail product is $1 + O (1/ D_{0})$ , and multiplying by $φ (W) / W$ gives the claim. ◻

6.7 The convolution defect and the asymptotic for $H$

Sublemma 6.33 (Size of the convolution defect). Let $b$ be the convolution defect of Definition 4.8. For every prime $p ∤ V$ , $∣ b (p) ∣ \leq \frac{2 A _{3}}{A _{1}} \cdot \frac{1}{p ^{2}} .$

Lean: PrimeGaps.SieveDatum.bDefect_bound

Uses: Definition 4.3, Definition 4.8, Definition 4.4

Proof. Fix a prime $p ∤ V$ . The structural hypothesis of Definition 4.3 gives $∣ γ (p) - 1∣ \leq A_{3} / p$ , and Lemma 4.5 gives $p - γ (p) \geq A_{1} p$ . Then $b (p) = \frac{γ ( p )}{p - γ ( p )} - \frac{1}{p - 1} = \frac{p ( γ ( p ) - 1 )}{( p - γ ( p ) ) ( p - 1 )},$ so, using $p - 1 \geq p /2$ , $∣ b (p) ∣ \leq \frac{p \cdot A _{3} / p}{A _{1} p \cdot p /2} = \frac{2 A _{3}}{A _{1} p ^{2}} .$ ◻

Proof uses: Lemma 4.5

Definition 6.34 (The normalised defect $b ~$ ). With $b$ as in Definition 4.8, set $b ~ (e) := b (e) \frac{φ ( e )}{e} (e \geq 1) .$ Like $b$ , the function $b ~$ is multiplicative and supported on squarefree integers coprime to $V$ , and $∣ b ~ (e) ∣ \leq ∣ b (e) ∣$ because $φ (e) / e \in [0, 1]$ .

Uses: Definition 4.8, Definition 3.4

Sublemma 6.35 (Uniform summability of the defect). There is a function $K = K (A_{1}, A_{3}) > 0$ , depending only on $A_{1}$ and $A_{3}$ , such that for every sieve datum with those parameters $e \geq 1 \sum ∣ b (e) ∣ τ (e) e \leq K (A_{1}, A_{3}) .$

Uses: Definition 4.3, Definition 4.8, Sublemma 6.33

Proof. The function $e \mapsto ∣ b (e) ∣ τ (e) e$ is non-negative, multiplicative, supported on squarefree $e$ , and takes the value $1$ at $e = 1$ . Hence its sum over all $e$ equals the Euler product $\prod_{p} (1 + ∣ b (p) ∣ τ (p) p)$ , the primes dividing $V$ contributing the factor $1$ . For $p ∤ V$ , Sublemma 6.33 and $τ (p) = 2$ give $∣ b (p) ∣ τ (p) p \leq \frac{4 A _{3}}{A _{1}} \cdot \frac{1}{p ^{3/2}} .$ Since $\sum_{p} p^{- 3/2}$ converges, $lo g \prod_{p} (1 + \cdot) \leq \sum_{p} ∣ b (p) ∣ τ (p) p \leq (4 A_{3} / A_{1}) \sum_{p} p^{- 3/2}$ , and exponentiating gives a bound depending only on $A_{1}$ and $A_{3}$ . (In particular the sum is finite, so the Euler factorisation used above is legitimate.) ◻

Proof uses: Sublemma 6.33

Sublemma 6.36 (Convolution identity for $h$ ). Let $h$ be as in Definition 4.6, and let $a : N \to R$ satisfy $a (n) = μ (n)^{2} / φ (n)$ for every $n$ . For every squarefree $d \geq 1$ with $(d, V) = 1$ , $h (d) = e ∣ d \sum b (e) a (d / e) .$

Lean: PrimeGaps.SieveDatum.h_eq_sum_bDefect_mul_a

Uses: Definition 4.6, Definition 4.8, Definition 4.4, Definition 3.4, Definition 3.3

Proof. For squarefree $d$ , each divisor $e ∣ d$ is squarefree and coprime to $d / e$ , so the right-hand side is the value at $d$ of the Dirichlet convolution of two multiplicative functions restricted to squarefree arguments; it therefore factors as $\prod_{p ∣ d} (b (p) + a (p))$ , each prime going wholly into $e$ or into $d / e$ . Since $(d, V) = 1$ , every $p ∣ d$ satisfies $p ∤ V$ , so $a (p) = 1/ (p - 1)$ and $b (p) + a (p) = g_{*} (p)$ by Definition 4.8. Hence the product equals $\prod_{p ∣ d} g_{*} (p) = g_{*} (d) = μ (d)^{2} g_{*} (d) = h (d)$ , using total multiplicativity of $g_{*}$ and $μ (d)^{2} = 1$ . ◻

Sublemma 6.37 (Convolution form of $H$ ). Let $H$ be as in Definition 4.28. For every real $z$ , $H (z) = e \geq 1 \sum b (e) 0 < f < z / e (f, V e) = 1 \sum \frac{μ ( f ) ^{2}}{φ ( f )},$ the $e$ -sum having only finitely many non-zero terms (those with $e < z$ ).

Uses: Definition 4.28, Definition 4.6, Definition 4.8, Sublemma 6.36, Definition 6.21

Proof. First, $h$ is supported on integers coprime to $V$ : this is Lemma 4.7, whose proof is that for $p ∣ V$ the structural hypothesis gives $γ (p) = 0$ , hence $g_{*} (p) = 0$ , and total multiplicativity of $g_{*}$ forces $h (d) = μ (d)^{2} g_{*} (d) = 0$ whenever $(d, V) > 1$ . Therefore $H (z) = \sum_{0 < d < z, (d, V) = 1} h (d)$ , and only squarefree $d$ contribute.

Now insert Sublemma 6.36 and exchange the order of the two finite sums, grouping by the divisor $e$ : $H (z) = 0 < d < z (d, V) = 1, d squarefree \sum e ∣ d \sum b (e) a (d / e) = e \geq 1 \sum b (e) 0 < f < z / e (f, V e) = 1 \sum a (f),$ where $f = d / e$ : the constraints “ $d < z$ , $e ∣ d$ ” become “ $f < z / e$ ”, while “ $d$ squarefree, $(d, V) = 1$ ” becomes “ $e$ squarefree coprime to $V$ ” (already enforced by the support of $b$ ) together with “ $f$ squarefree, $(f, V e) = 1$ ” (the condition $(f, e) = 1$ being enforced by $μ (f)^{2}$ inside $a (f)$ when combined with the squarefreeness of $d = e f$ ). Terms with $e \geq z$ have empty inner sum. ◻

Proof uses: Sublemma 6.36, Lemma 4.7, Definition 4.4, Definition 4.3

Sublemma 6.38 (Euler-product identification of $S (γ)$ ). For every sieve datum, $S (γ) = \frac{φ ( V )}{V} e \geq 1 \sum b ~ (e),$ the series converging absolutely. In particular $S (γ) > 0$ .

Uses: Notation 3.41, Definition 6.34, Definition 4.3, Sublemma 6.35

Proof. Absolute convergence follows from $∣ b ~ (e) ∣ \leq ∣ b (e) ∣ \leq ∣ b (e) ∣ τ (e) e$ and Sublemma 6.35. Since $b ~$ is multiplicative, supported on squarefree integers coprime to $V$ , the sum factors as $\sum_{e \geq 1} b ~ (e) = \prod_{p ∤ V} (1 + b ~ (p))$ . For $p ∤ V$ , $1 + b ~ (p) = 1 + \frac{p - 1}{p} (g_{*} (p) - \frac{1}{p - 1}) = \frac{p - 1}{p} (1 + g_{*} (p)) = (1 - \frac{1}{p}) (1 - \frac{γ ( p )}{p})^{- 1},$ using $1 + g_{*} (p) = 1 + γ (p) / (p - γ (p)) = (1 - γ (p) / p)^{- 1}$ . These are exactly the local factors of $S (γ)$ (Notation 3.41) at the primes $p ∤ V$ . At the primes $p ∣ V$ one has $γ (p) = 0$ , so the local factor of $S (γ)$ is $1 - 1/ p$ , and $\prod_{p ∣ V} (1 - 1/ p) = φ (V) / V$ . Multiplying the two contributions gives the identity. Positivity holds because each local factor is positive and the product converges. ◻

Proof uses: Sublemma 6.35, Definition 4.4, Definition 6.34

Sublemma 6.39 (Asymptotic for $H$ ). There are functions $C_{1} = C_{1} (A_{1}, A_{3}) > 0$ and $C_{2} = C_{2} (A_{1}, A_{3}) > 0$ such that, for every sieve datum with parameters $A_{1}, A_{2}, A_{3}, L$ and every real $z \geq 2$ , $H (z) - S (γ) lo g z \leq C_{1} S (γ) (1 + ℓ_{V}) + C_{2} τ (V) z^{- 1/8} lo g (2 V z) .$ Both constants depend on $A_{1}$ and $A_{3}$ only; neither depends on $A_{2}$ , $L$ , $γ$ , $V$ or $z$ .

Lean: PrimeGaps.slem_H_error_assembly

Uses: Definition 4.28, Definition 4.3, Notation 3.41, Definition 6.18, Sublemma 6.37, Sublemma 6.22, Sublemma 6.35, Sublemma 6.38, Definition 6.34

Proof. Throughout, all implied constants depend on $A_{1}, A_{3}$ only. Write $A (x; m) := \sum_{0 < f < x, (f, m) = 1} μ (f)^{2} / φ (f)$ for the strict truncation appearing in Sublemma 6.37; it differs from $A_{m} (x)$ of Definition 6.21 by at most one term $μ (f)^{2} / φ (f) ≪ x^{- 1/2}$ , so Sublemma 6.22 applies to $A$ with the same error shape.

Preliminaries on $b ~$ . From $∣ b ~ (e) ∣ \leq ∣ b (e) ∣$ and Sublemma 6.35, $e \sum ∣ b ~ (e) ∣ τ (e) e^{1/2} e \sum ∣ b ~ (e) ∣ e^{1/4} e \sum ∣ b ~ (e) ∣ (1 + lo g e) = = = O (1), O (1), O (1),$ the second and third following from the first by $e^{1/4} \leq τ (e) e^{1/2}$ and $1 + lo g e \leq 3 τ (e) e^{1/2}$ .

Step 1: main range $e \leq z$ . For such $e$ we have $z / e \geq z \geq 2$ , so Sublemma 6.22 applies with $m = V e$ . Using $(e, V) = 1$ , so that $φ (V e) / (V e) = (φ (V) / V) (φ (e) / e)$ and $ℓ_{V e} = ℓ_{V} + ℓ_{e}$ , and $b (e) φ (e) / e = b ~ (e)$ , $e \leq z (e, V) = 1 \sum b (e) A (z / e; V e) = \frac{φ ( V )}{V} e \leq z (e, V) = 1 \sum b ~ (e) (lo g z - lo g e + ℓ_{V} + ℓ_{e}) + O (\frac{φ ( V )}{V}) + R (z),$ where the $O (φ (V) / V)$ collects the $O (φ (V e) / (V e))$ errors against $\sum_{e} ∣ b ~ (e) ∣ = O (1)$ , and $R (z) := e \leq z (e, V) = 1 \sum b (e) O (\frac{τ ( V e ) lo g ( 2 V ez )}{z / e}) = O (τ (V) z^{- 1/2} lo g (2 V z) e \sum ∣ b (e) ∣ τ (e) e^{1/2}),$ which is $O (τ (V) z^{- 1/2} lo g (2 V z))$ by Sublemma 6.35 (using $τ (V e) = τ (V) τ (e)$ for $(e, V) = 1$ ).

Step 2: complete the $e$ -sum. Extend the sum to all $e$ coprime to $V$ . The discarded range $e > z$ is controlled by $∣ lo g z - lo g e + ℓ_{V} + ℓ_{e} ∣ ≪ lo g (2 z) + ℓ_{V} + lo g e$ together with $\sum_{e > z} ∣ b ~ (e) ∣ \leq z^{- 1/8} \sum_{e} ∣ b ~ (e) ∣ e^{1/4} = O (z^{- 1/8})$ and the same estimate with an extra $lo g e$ ; this gives an error $O (\frac{φ ( V )}{V} z^{- 1/8} (lo g 2 z + ℓ_{V}))$ . Similarly the tail $e > z$ of the true sum of Sublemma 6.37 is $O (\frac{φ ( V )}{V} z^{- 1/8} lo g 2 z)$ , since $A (z / e; V e) ≪ \frac{φ ( V )}{V} lo g (2 z)$ trivially.

For the completed sum, split $lo g z - lo g e + ℓ_{V} + ℓ_{e}$ . By Sublemma 6.38, $\frac{φ ( V )}{V} \sum_{(e, V) = 1} b ~ (e) = S (γ)$ , so the $lo g z$ and $ℓ_{V}$ parts produce $S (γ) (lo g z + ℓ_{V})$ . The remaining part is $\frac{φ ( V )}{V} (e, V) = 1 \sum b ~ (e) (ℓ_{e} - lo g e) ≪ \frac{φ ( V )}{V} e \sum ∣ b ~ (e) ∣ (1 + lo g e) = O (\frac{φ ( V )}{V}),$ using $0 \leq ℓ_{e} \leq lo g e$ for $e \geq 1$ .

Step 3: comparison of $φ (V) / V$ with $S (γ)$ . By Sublemma 6.38 and $\sum_{e} ∣ b ~ (e) ∣ = O (1)$ we get $S (γ) ≪ φ (V) / V$ ; conversely, the local factors at $p ∤ V$ satisfy $lo g (1 + b ~ (p)) \geq - 2 A_{3} / p^{2}$ by Sublemma 6.33, so $\prod_{p ∤ V} (1 + b ~ (p)) \geq exp (- 2 A_{3} \sum_{p} p^{- 2}) ≫ 1$ and hence $φ (V) / V ≪ S (γ)$ . The two quantities are therefore comparable, with constants depending on $A_{1}, A_{3}$ only, and every $O (φ (V) / V)$ above may be rewritten as $O (S (γ))$ , hence absorbed into $O (S (γ) (1 + ℓ_{V}))$ .

Collecting Steps 1–3 and noting $z^{- 1/2} \leq z^{- 1/8}$ and $lo g (2 V z) \geq 1$ for $z \geq 2$ , $V \geq 1$ , the two error shapes of the statement are obtained. ◻

Proof uses: Sublemma 6.37, Sublemma 6.22, Sublemma 6.35, Sublemma 6.38, Sublemma 6.33, Definition 6.21, Definition 6.18

6.8 Partial summation

Sublemma 6.40 (Cost of the removed primes). There is a function $C = C (A_{3}) > 0$ such that, for every sieve datum with parameters $A_{1}, A_{2}, A_{3}, L$ , $ℓ_{V} = p ∣ V \sum \frac{lo g p}{p - 1} \leq 2 L + C (A_{3}) .$

Lean: PrimeGaps.ellV_le_two_L_add_const

Uses: Definition 4.3, Definition 6.18, Lemma 6.7

Proof. Fix $z \geq max {p : p ∣ V}$ (and $z \geq 2$ ). Since $γ (p) = 0$ for $p ∣ V$ , $2 \leq p \leq z \sum \frac{γ ( p ) lo g p}{p} = p \leq z p ∤ V \sum \frac{lo g p}{p} + p \leq z p ∤ V \sum \frac{( γ ( p ) - 1 ) lo g p}{p} .$ By the structural hypothesis the second sum is at most $A_{3} \sum_{p} (lo g p) / p^{2} = O_{A_{3}} (1)$ in absolute value, the series converging. For the first, Mertens’ first theorem $\sum_{p \leq z} (lo g p) / p = lo g z + O (1)$ (Lemma 6.7, after discarding the proper prime powers) gives $2 \leq p \leq z \sum \frac{γ ( p ) lo g p}{p} = lo g z - p ∣ V \sum \frac{lo g p}{p} + O_{A_{3}} (1) .$ The lower half of the log-sum hypothesis at $w = 2$ reads $\sum_{2 \leq p \leq z} γ (p) (lo g p) / p \geq lo g (z /2) - L$ . Subtracting yields $\sum_{p ∣ V} (lo g p) / p \leq L + O_{A_{3}} (1)$ . Finally $p / (p - 1) \leq 2$ for every prime $p$ , so $ℓ_{V} \leq 2 \sum_{p ∣ V} (lo g p) / p \leq 2 L + O_{A_{3}} (1)$ . ◻

Lemma 6.41 (Partial summation). There are functions $C_{1} = C_{1} (A_{1}, A_{2}, A_{3}) > 0$ and $C_{2} = C_{2} (A_{1}, A_{3}) > 0$ such that the following holds for every sieve datum with parameters $A_{1}, A_{2}, A_{3}, L$ , every continuously differentiable $G : R \to R$ , and every real $z \geq 2$ : $0 < d < z \sum μ (d)^{2} g_{*} (d) G (\frac{lo g d}{lo g z}) - S (γ) (lo g z) \int_{0}^{1} G (x) d x \leq C_{1} S (γ) L G_{m a x} + C_{2} \frac{τ ( V ) lo g ( 2 V z )}{lo g z} G_{m a x},$ where $G_{m a x} = sup_{t \in [0, 1]} (∣ G (t) ∣ + ∣ G^{'} (t) ∣)$ .

Lean: PrimeGaps.lem_partial_sum

Uses: Definition 4.3, Definition 4.4, Definition 4.6, Definition 4.28, Notation 3.41, Sublemma 6.39, Sublemma 6.40

Proof. Write $S (z) := \sum_{0 < d < z} h (d) G (lo g d / lo g z)$ with $h (d) = μ (d)^{2} g_{*} (d)$ .

Step 1: Abel summation. The function $H$ of Definition 4.28 is the summatory function of $h$ ; taking $ψ (t) := G (lo g t / lo g z)$ , so that $ψ^{'} (t) = G^{'} (lo g t / lo g z) / (t lo g z)$ and $ψ (z) = G (1)$ , Abel summation gives the exact identity $S (z) = G (1) H (z) - \int_{1}^{z} \frac{G ^{'} ( lo g t / lo g z )}{t lo g z} H (t) d t .$ (The integrand is continuous off the integers and $H$ is a bounded monotone step function on $[1, z]$ , so the integral exists.)

Step 2: separate main term and error. Write $H (t) = S (γ) lo g t + r (t)$ . For the main term, substitute $x := lo g t / lo g z$ , so $d x = d t / (t lo g z)$ and $lo g t = x lo g z$ : $S (γ) \int_{1}^{z} \frac{G ^{'} ( lo g t / lo g z )}{t lo g z} lo g t d t = S (γ) (lo g z) \int_{0}^{1} x G^{'} (x) d x .$ Integration by parts gives $\int_{0}^{1} x G^{'} (x) d x = G (1) - \int_{0}^{1} G (x) d x$ , so together with the boundary contribution $G (1) S (γ) lo g z$ the main terms combine to exactly $S (γ) (lo g z) \int_{0}^{1} G (x) d x$ . Consequently $S (z) - S (γ) (lo g z) \int_{0}^{1} G \leq G_{m a x} (∣ r (z) ∣ + \frac{1}{lo g z} \int_{1}^{z} \frac{∣ r ( t ) ∣}{t} d t),$ using $∣ G (1) ∣ \leq G_{m a x}$ and $∣ G^{'} ∣ \leq G_{m a x}$ on $[0, 1]$ .

Step 3: bound the error functional. By Sublemma 6.39, $∣ r (t) ∣ \leq C_{1}^{'} S (γ) (1 + ℓ_{V}) + C_{2}^{'} τ (V) t^{- 1/8} lo g (2 V t) (2 \leq t \leq z),$ with $C_{1}^{'}, C_{2}^{'}$ depending on $A_{1}, A_{3}$ ; on $[1, 2]$ one has $∣ H (t) ∣ \leq 1$ and $S (γ) lo g t \leq S (γ) lo g 2$ , so the same shape holds after enlarging the constants. The first piece integrates to $O (S (γ) (1 + ℓ_{V}))$ (since $\frac{1}{l o g z} \int_{1}^{z} d t / t = 1$ ), and the second to $O (τ (V) lo g (2 V) / lo g z)$ , because $\int_{1}^{\infty} t^{- 9/8} lo g (2 V t) d t = O (lo g 2 V)$ is a convergent integral. The boundary term $∣ r (z) ∣$ is dominated by the same two shapes, using $z^{- 1/8} \leq 1/ lo g z$ for $z \geq 2$ .

Step 4: collapse $ℓ_{V}$ to $L$ . By Sublemma 6.40, $1 + ℓ_{V} \leq 1 + 2 L + C (A_{3})$ . Absorbing the additive constants (the $A_{2}$ -dependence entering through the parameter $L$ supplied by the log-sum hypothesis) turns $S (γ) (1 + ℓ_{V})$ into $C_{1} (A_{1}, A_{2}, A_{3}) S (γ) L$ plus a term of the second shape. Multiplying through by $G_{m a x}$ gives the stated bound. ◻

Proof uses: Sublemma 6.39, Sublemma 6.40, Definition 6.18, Definition 4.28

7 Relating the transformed weight systems

The sieve analysis uses four systems of variables: the profile $F$ , the divisor weights $λ (d_{1}, \dots, d_{k})$ , the $y$ -variables $y (r_{1}, \dots, r_{k})$ (Definition 4.20), and, for each $m \in {1, \dots, k}$ , the $m$ -th marginal variables $y^{(m)} (r_{1}, \dots, r_{k})$ (Definition 4.25). The $S_{1} (λ)$ analysis is carried out in the $y$ -variables and the $S_{2}^{(m)} (λ)$ analysis in the $y^{(m)}$ -variables; both are evaluated in terms of $F$ . This section relates them: the $y$ -variables of the $F$ -derived sieve weight are evaluated in closed form, and $y^{(m)}$ is expressed in terms of $y$ up to an error of relative size $1/ D_{0}$ .

Throughout, $k \geq 2$ is fixed, $λ : N^{k} \to R$ is a function of finite support, $y$ denotes the $y$ -transform of $λ$ (Definition 4.20) and $y^{(m)}$ the $m$ -th marginal transform (Definition 4.25). The parameters $D_{0}$ , $W$ and $R$ are those of Definitions 3.28, 3.29 and 3.37, and “permissible support” always means Definition 3.39.

7.1 Finiteness of the marginal supremum

Lemma 7.1 ( $y_{m a x}^{(m)}$ is a finite maximum). Let $m \in {1, \dots, k}$ and let $λ : N^{k} \to R$ be a function of finite support. Then $y_{m a x}^{(m)} < \infty$ ; in fact the supremum is attained as a maximum on a finite subset of $N^{k}$ .

Lean: PrimeGaps.ymMax_finite

Uses: Definition 4.25, Definition 4.27

Proof. Suppose $y^{(m)} (r_{1}, \dots, r_{k}) \neq = 0$ . By Definition 4.25 the defining $d$ -sum has a nonzero summand, so there is a tuple $d = (d_{1}, \dots, d_{k}) \in supp (λ)$ with $r_{i} ∣ d_{i}$ for every $i$ ; in particular $r_{i} \leq d_{i}$ for every $i$ . Since $λ$ has finite support, the integer $M := max {d_{i} : d \in supp (λ), 1 \leq i \leq k}$ is well defined and finite, and every $r$ with $y^{(m)} (r) \neq = 0$ lies in the finite set ${1, \dots, M}^{k}$ . Hence $y_{m a x}^{(m)} = max {∣ y^{(m)} (r) ∣ : r \in {1, \dots, M}^{k}}$ is a maximum over a finite set, and is finite. ◻

7.2 The $y$ -variables of the $F$ -derived weight

Lemma 7.2 (The transform of the $F$ -derived weight is exactly $y_{0}$ ). Let $R > 0$ , let $W \geq 1$ , and let $F : R^{k} \to R$ be arbitrary. Let $y_{0}$ be the $F$ -derived $y$ -weight of Definition 5.5 and let $λ_{0}$ be the associated sieve weight of Definition 5.6. Then the $y$ -transform of $λ_{0}$ (Definition 4.20) is $y_{0}$ : $y_{λ_{0}} (r_{1}, \dots, r_{k}) = y_{0} (r_{1}, \dots, r_{k}) for every (r_{1}, \dots, r_{k}) \in N^{k} .$

Lean: PrimeGaps.lem_y_from_lambda_0

Uses: Definition 5.5, Definition 5.6, Definition 4.20

Proof. By Definition 5.6 the weight $λ_{0}$ is the Möbius transform $λ_{y_{0}}$ of $y_{0}$ (Definition 4.22). The round-trip identity Lemma 4.24 therefore gives $y_{λ_{0}} (r) = y_{λ_{y_{0}}} (r) = {y_{0} (r) 0 if r_{i} is squarefree for every i, otherwise.$ It remains to check that $y_{0} (r) = 0$ whenever some $r_{i}$ fails to be squarefree. In that case $\prod_{j} r_{j}$ is not squarefree, so $r$ does not lie in the permissible support of Definition 3.39; since $y_{0}$ is by construction supported there (Definition 5.5), $y_{0} (r) = 0$ . Both sides therefore agree at every $r$ . ◻

Proof uses: Definition 5.6, Lemma 4.24, Definition 4.22, Definition 3.39

Lemma 7.3 (Piecewise closed form of $y$ for the $F$ -derived sieve weight). Let $k \geq 2$ , let $R > 0$ , let $W \geq 1$ , and let $F : R^{k} \to R$ be a smooth function with $supp F \subseteq R_{k}$ (Definition 5.1). Let $λ_{0}$ be the $F$ -derived sieve weight of Definition 5.6 and let $y$ be its $y$ -transform (Definition 4.20). Then, for every $(r_{1}, \dots, r_{k}) \in N^{k}$ , $y (r_{1}, \dots, r_{k}) = {F (\frac{l o g r _{1}}{l o g R}, \dots, \frac{l o g r _{k}}{l o g R}) 0 if \prod_{i = 1}^{k} r_{i} is squarefree and g cd (\prod_{i = 1}^{k} r_{i}, W) = 1, otherwise.$

Lean: PrimeGaps.y_from_lambda

Uses: Definition 5.6, Definition 4.20, Definition 5.1, Definition 3.37, Definition 3.29

Proof. By Lemma 7.2, $y = y_{0}$ , and by Definition 5.5, $y_{0} (r) = F (\frac{l o g r _{1}}{l o g R}, \dots, \frac{l o g r _{k}}{l o g R}) \cdot 1 [r lies in the permissible support] .$ The permissible support consists of the tuples satisfying the three conditions $\prod_{i} r_{i} \leq R$ , $g cd (\prod_{i} r_{i}, W) = 1$ , and $\prod_{i} r_{i}$ squarefree (Definition 3.39). Two of these are exactly the conditions in the assertion, so it suffices to prove that the truncation condition is automatic: precisely, that $F (\frac{l o g r _{1}}{l o g R}, \dots, \frac{l o g r _{k}}{l o g R}) \neq = 0 and \prod_{i} r_{i} squarefree ⟹ \prod_{i} r_{i} \leq R .$ Assume the left-hand side and write $x_{i} := lo g r_{i} / lo g R$ . Squarefreeness of $\prod_{i} r_{i}$ forces $r_{i} \geq 1$ for every $i$ , so $lo g r_{i} \geq 0$ . Since $F$ is nonzero at $x = (x_{1}, \dots, x_{k})$ and $supp F \subseteq R_{k}$ , we have $x \in R_{k}$ , i.e. $x_{i} \geq 0$ for every $i$ and $\sum_{i} x_{i} \leq 1$ .

If $lo g R > 0$ , then $\sum_{i} x_{i} \leq 1$ reads $\sum_{i} lo g r_{i} \leq lo g R$ , that is, $lo g (\prod_{i} r_{i}) \leq lo g R$ ; exponentiating gives $\prod_{i} r_{i} \leq R$ , as required.

If instead $lo g R \leq 0$ (that is, $0 < R \leq 1$ ), then each $x_{i} = lo g r_{i} / lo g R$ is a quotient of a non-negative number by a non-positive one, hence $x_{i} \leq 0$ ; combined with $x_{i} \geq 0$ this gives $x = 0$ . But $F (0) = 0$ : since $k \geq 1$ , the origin is a limit of points outside $R_{k}$ (move along a single coordinate ray into negative values), $F$ vanishes identically off $R_{k}$ , and $F$ is continuous, so $F (0) = 0$ by continuity. This contradicts $F (x) \neq = 0$ , so the case is vacuous. In either case the implication holds, and the piecewise formula follows. ◻

Proof uses: Lemma 7.2, Definition 5.5, Definition 3.39

Definition 7.4 ( $C^{1}$ -norm $F_{m a x}$ on $[0, 1]^{k}$ ). For a $C^{1}$ function $F : R^{k} \to R$ , set $F_{m a x} := t \in [0, 1]^{k} sup (∣ F (t) ∣ + i = 1 \sum k \frac{\partial F}{\partial t _{i}} (t)) .$ The supremum is over the compact unit cube, on which the displayed function is continuous, so it is finite; it is non-negative because the quantity inside the supremum is non-negative.

7.3 Expressing $y^{(m)}$ through $y$

Lemma 7.5 (Substitute the inversion formula for $λ$ into $y^{(m)}$ ). Let $λ$ have permissible support, let $m \in {1, \dots, k}$ , and let $r \in N^{k}$ satisfy $r_{m} = 1$ . Then $y^{(m)} (r_{1}, \dots, r_{k}) = (i = 1 \prod k μ (r_{i}) g (r_{i})) d \in N^{k} r_{i} ∣ d_{i} \forall i, d_{m} = 1 \sum (i = 1 \prod k \frac{μ ( d _{i} ) d _{i}}{φ ( d _{i} )}) a \in N^{k} d_{i} ∣ a_{i} \forall i \sum \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )},$ both sums running over tuples of positive integers.

Lean: PrimeGaps.MaynardSubstitute.lem_ym_substitute_y

Uses: Definition 4.25, Definition 4.20, Definition 3.39, Definition 3.3, Definition 3.6, Definition 3.4

Proof. By Definition 4.25, $y^{(m)} (r_{1}, \dots, r_{k}) = (i = 1 \prod k μ (r_{i}) g (r_{i})) d r_{i} ∣ d_{i} \forall i, d_{m} = 1 \sum \frac{λ ( d _{1} , \dots , d _{k} )}{\prod _{i = 1}^{k} φ ( d _{i} )},$ a finite sum because $λ$ has finite support; moreover every contributing $d$ has $\prod_{i} d_{i}$ squarefree, hence positive squarefree coordinates, by Definition 3.39. On such tuples Lemma 4.23 identifies $λ$ with the Möbius transform of its own $y$ -variables (Definition 4.22): $λ (d) = (i = 1 \prod k μ (d_{i}) d_{i}) a d_{i} ∣ a_{i} \forall i \sum \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )} .$ Dividing by $\prod_{i} φ (d_{i})$ gives $\frac{λ ( d )}{\prod _{i = 1}^{k} φ ( d _{i} )} = (i = 1 \prod k \frac{μ ( d _{i} ) d _{i}}{φ ( d _{i} )}) a d_{i} ∣ a_{i} \forall i \sum \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )},$ and inserting this into the previous display yields the asserted formula. (The hypothesis $r_{m} = 1$ is not used in the derivation; it is recorded because $y^{(m)}$ vanishes otherwise, by Lemma 4.26.) ◻

Proof uses: Lemma 4.23, Definition 4.22, Lemma 4.26

Lemma 7.6 (Interchange the $d$ - and $a$ -summations). Let $λ$ have permissible support, let $m \in {1, \dots, k}$ , and let $r \in N^{k}$ satisfy $r_{i} \geq 1$ for every $i$ and $r_{m} = 1$ . Then $y^{(m)} (r_{1}, \dots, r_{k}) = (i = 1 \prod k μ (r_{i}) g (r_{i})) a \in N^{k} r_{i} ∣ a_{i} \forall i \sum \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )} d \in N^{k} r_{i} ∣ d_{i} ∣ a_{i} \forall i, d_{m} = 1 \sum i = 1 \prod k \frac{μ ( d _{i} ) d _{i}}{φ ( d _{i} )} .$

Lean: PrimeGaps.lem_ym_swap

Uses: Definition 4.25, Definition 4.20, Definition 3.39, Definition 3.3, Definition 3.6, Definition 3.4

Proof. The iterated sum of Lemma 7.5 is supported on the set of pairs $(d, a)$ with $r_{i} ∣ d_{i} ∣ a_{i}$ for every $i$ and $d_{m} = 1$ : the outer summation imposes $r_{i} ∣ d_{i}$ and $d_{m} = 1$ , and the inner one imposes $d_{i} ∣ a_{i}$ , which together force $r_{i} ∣ a_{i}$ . Both summations are finite, since $y$ has finite support (Definition 4.20) and, for fixed $a$ , only the finitely many divisor tuples $d$ of $a$ contribute. We may therefore interchange the order of summation: grouping first by $a$ , the inner $d$ -sum runs over ${d : r_{i} ∣ d_{i} ∣ a_{i} \forall i, d_{m} = 1}$ . Multiplying by the outer prefactor $\prod_{i} μ (r_{i}) g (r_{i})$ , which depends only on $r$ , gives the asserted identity. ◻

Proof uses: Lemma 7.5

Lemma 7.7 (Evaluation of the inner divisor sum). Let $a$ be a positive squarefree integer and let $r$ be a positive divisor of $a$ . Then $d ∣ a r ∣ d \sum \frac{μ ( d ) d}{φ ( d )} = \frac{μ ( a ) r}{φ ( a )} .$

Lean: PrimeGaps.lem_ym_eval_d_sum

Uses: Definition 3.3, Definition 3.4

Proof. Write $a = r e$ with $e := a / r$ . Since $a$ is squarefree, so are $r$ and $e$ , and $(r, e) = 1$ .

Every $d$ with $r ∣ d ∣ a$ is uniquely of the form $d = r f$ with $f ∣ e$ , and then $(r, f) = 1$ , so by multiplicativity of $μ$ and of $φ$ on coprime products, $μ (d) = μ (r) μ (f)$ and $φ (d) = φ (r) φ (f)$ . Substituting, $d ∣ a r ∣ d \sum \frac{μ ( d ) d}{φ ( d )} = \frac{μ ( r ) r}{φ ( r )} f ∣ e \sum \frac{μ ( f ) f}{φ ( f )} .$ The summand $f \mapsto μ (f) f / φ (f)$ is multiplicative, so for squarefree $e$ the divisor sum factors over the prime divisors of $e$ : $f ∣ e \sum \frac{μ ( f ) f}{φ ( f )} = p ∣ e \prod (1 + \frac{μ ( p ) p}{φ ( p )}) = p ∣ e \prod (1 - \frac{p}{p - 1}) = p ∣ e \prod \frac{- 1}{p - 1} = \frac{( - 1 ) ^{ω (e)}}{\prod _{p ∣ e} ( p - 1 )} = \frac{μ ( e )}{φ ( e )},$ using $μ (e) = (- 1)^{ω (e)}$ and $φ (e) = \prod_{p ∣ e} (p - 1)$ for squarefree $e$ . Combining the two displays, $d ∣ a r ∣ d \sum \frac{μ ( d ) d}{φ ( d )} = \frac{μ ( r ) μ ( e ) r}{φ ( r ) φ ( e )} = \frac{μ ( a ) r}{φ ( a )},$ the last step again by multiplicativity of $μ$ and $φ$ on the coprime product $a = r e$ . ◻

Lemma 7.8 ( $y^{(m)}$ in terms of $y$ , intermediate form). Let $λ$ have permissible support, let $m \in {1, \dots, k}$ , and let $r \in N^{k}$ satisfy $r_{i} \geq 1$ for every $i$ and $r_{m} = 1$ . Then $y^{(m)} (r_{1}, \dots, r_{k}) = (i = 1 \prod k μ (r_{i}) g (r_{i})) a \in N^{k} r_{i} ∣ a_{i} \forall i \sum \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )} i \neq = m \prod \frac{μ ( a _{i} ) r _{i}}{φ ( a _{i} )} .$

Lean: PrimeGaps.lem_ym_intermediate

Uses: Definition 4.25, Definition 4.20, Definition 3.39, Definition 3.3, Definition 3.6, Definition 3.4

Proof. Start from Lemma 7.6 and evaluate, for each fixed $a$ , the inner sum $Σ (a) := d r_{i} ∣ d_{i} ∣ a_{i} \forall i, d_{m} = 1 \sum i = 1 \prod k \frac{μ ( d _{i} ) d _{i}}{φ ( d _{i} )} .$ It suffices to treat those $a$ with $y (a) \neq = 0$ ; by Lemma 4.21 such an $a$ has $\prod_{i} a_{i}$ squarefree, so every $a_{i}$ is positive and squarefree. The constraints on $d$ are coordinatewise, so $Σ (a)$ factors as a product over $i$ . The $m$ -th factor is $1$ : the constraint $d_{m} = 1$ leaves the single term $μ (1) \cdot 1/ φ (1) = 1$ , and $r_{m} = 1$ is compatible with it. For $i \neq = m$ the $i$ -th factor is $\sum_{r_{i} ∣ d_{i} ∣ a_{i}} μ (d_{i}) d_{i} / φ (d_{i})$ , which equals $μ (a_{i}) r_{i} / φ (a_{i})$ by Lemma 7.7 applied with $a = a_{i}$ and $r = r_{i}$ (legitimate since $a_{i}$ is squarefree and $r_{i} ∣ a_{i}$ ). Hence $Σ (a) = \prod_{i \neq = m} μ (a_{i}) r_{i} / φ (a_{i})$ , and substituting this into Lemma 7.6 gives the assertion. ◻

Proof uses: Lemma 7.6, Lemma 7.7, Lemma 4.21

7.4 The diagonal decomposition of $y^{(m)}$

Definition 7.9 (The $y^{(m)}$ -summand $T_{m, r}$ ). Let $m \in {1, \dots, k}$ and $r \in N^{k}$ . For $a \in N^{k}$ set $T_{m, r} (a) := (i = 1 \prod k μ (r_{i}) g (r_{i})) \cdot \frac{y ( a _{1} , \dots , a _{k} )}{\prod _{i = 1}^{k} φ ( a _{i} )} \cdot i \neq = m \prod \frac{μ ( a _{i} ) r _{i}}{φ ( a _{i} )},$ with the convention that the whole expression is read as $0$ when some $a_{i} = 0$ .

Uses: Definition 4.20, Definition 3.3, Definition 3.6, Definition 3.4

Definition 7.10 (The free-coordinate marginal $Y^{(m)}$ ). Let $m \in {1, \dots, k}$ and $r \in N^{k}$ . Set $Y^{(m)} (r_{1}, \dots, r_{k}) := a \geq 1 \sum \frac{y ( r _{1} , \dots , r _{m - 1} , a , r _{m + 1} , \dots , r _{k} )}{φ ( a )},$ the sum running over the single free coordinate in the $m$ -th slot. Only finitely many terms are nonzero, because $y$ has finite support.

Uses: Definition 4.20, Definition 3.4

Lemma 7.11 (Diagonal and off-diagonal decomposition of $y^{(m)}$ ). Let $λ$ have permissible support, let $m \in {1, \dots, k}$ , and let $r \in N^{k}$ be such that every $r_{i}$ is positive and squarefree and $r_{m} = 1$ . Then $y^{(m)} (r_{1}, \dots, r_{k}) = (i \neq = m \prod \frac{g ( r _{i} ) r _{i}}{φ ( r _{i} ) ^{2}}) Y^{(m)} (r_{1}, \dots, r_{k}) + a \in N^{k} : r_{i} ∣ a_{i} \forall i \exists j \neq = m, a_{j} \neq = r_{j} \sum T_{m, r} (a) .$

Uses: Definition 4.25, Definition 7.9, Definition 7.10, Definition 3.39, Definition 3.6, Definition 3.4

Proof. By Lemma 7.8 and Definition 7.9, $y^{(m)} (r) = a r_{i} ∣ a_{i} \forall i \sum T_{m, r} (a),$ the sum being finite because $y$ has finite support and $T_{m, r}$ vanishes wherever $y$ does. Split the index set ${a : r_{i} ∣ a_{i} \forall i}$ into the diagonal part $D := {a : r_{i} ∣ a_{i} \forall i, a_{i} = r_{i} \forall i \neq = m}$ and its complement, the off-diagonal part $O := {a : r_{i} ∣ a_{i} \forall i, \exists j \neq = m, a_{j} \neq = r_{j}}$ . These are disjoint with union the whole index set, so the sum splits accordingly, and the second piece is the displayed off-diagonal sum.

It remains to evaluate the diagonal piece. Since $r_{m} = 1$ divides every integer, the tuples in $D$ are exactly those obtained from $r$ by replacing the $m$ -th coordinate by an arbitrary $a \geq 0$ , and distinct $a$ give distinct tuples. For such a tuple, using $φ (a_{i}) = φ (r_{i})$ and $μ (a_{i}) = μ (r_{i})$ for $i \neq = m$ , $T_{m, r} (a) = (μ (r_{m}) g (r_{m}) i \neq = m \prod μ (r_{i}) g (r_{i})) \cdot \frac{y ( a )}{φ ( a ) \prod _{i \neq = m} φ ( r _{i} )} \cdot i \neq = m \prod \frac{μ ( r _{i} ) r _{i}}{φ ( r _{i} )} .$ The factor $μ (r_{m}) g (r_{m})$ equals $1$ because $r_{m} = 1$ , and $μ (r_{i})^{2} = 1$ for each $i \neq = m$ because $r_{i}$ is squarefree. Collecting the $i \neq = m$ factors, $T_{m, r} (a) = (i \neq = m \prod \frac{g ( r _{i} ) r _{i}}{φ ( r _{i} ) ^{2}}) \cdot \frac{y ( a )}{φ ( a )} .$ Summing over $a \geq 1$ — the term $a = 0$ contributes $0$ by the convention of Definition 7.9 — and recognising Definition 7.10 gives the diagonal contribution $(\prod_{i \neq = m} g (r_{i}) r_{i} / φ (r_{i})^{2}) Y^{(m)} (r)$ , as asserted. ◻

Proof uses: Lemma 7.8, Definition 3.3

Lemma 7.12 (Approximation of the diagonal prefactor). There is a constant $C = C (k) \geq 0$ with the following property. Let $D_{0} \geq 2$ be real and let $r \in N^{k}$ be such that every $r_{i}$ is positive and squarefree and every prime factor of every $r_{i}$ exceeds $D_{0}$ . Then $i = 1 \prod k \frac{g ( r _{i} ) r _{i}}{φ ( r _{i} ) ^{2}} - 1 \leq \frac{C}{D _{0}} .$

Lean: PrimeGaps.lem_ym_prefactor

Uses: Definition 3.6, Definition 3.4, Definition 3.28

Proof. Fix $i$ . Since $r_{i}$ is squarefree, both $g$ and $φ$ factor over the distinct prime divisors of $r_{i}$ , and $\frac{g ( r _{i} ) r _{i}}{φ ( r _{i} ) ^{2}} = p ∣ r_{i} \prod \frac{( p - 2 ) p}{( p - 1 ) ^{2}} = p ∣ r_{i} \prod (1 - \frac{1}{( p - 1 ) ^{2}}),$ because $(p - 2) p = (p - 1)^{2} - 1$ . Hence $i = 1 \prod k \frac{g ( r _{i} ) r _{i}}{φ ( r _{i} ) ^{2}} x_{j} = := j \prod (1 - x_{j}), \frac{1}{( p _{j} - 1 ) ^{2}},$ where $p_{1}, p_{2}, \dots$ enumerates, with multiplicity, the prime divisors of $r_{1}, \dots, r_{k}$ . Every such prime exceeds $D_{0} \geq 2$ , so $p_{j} \geq 3$ and $0 \leq x_{j} \leq 1/4 \leq 1$ . For numbers $x_{j} \in [0, 1]$ one has the elementary bound $\prod_{j} (1 - x_{j}) - 1 \leq \sum_{j} x_{j}$ , proved by induction on the number of factors: if $P$ is a partial product then $0 \leq P \leq 1$ , so $∣ P (1 - x) - 1∣ \leq ∣ P - 1∣ + P x \leq ∣ P - 1∣ + x$ .

It therefore suffices to bound $\sum_{j} x_{j}$ . For a single index $i$ the primes $p ∣ r_{i}$ are distinct and all exceed $D_{0}$ , and $p - 1 \geq p /2$ for every prime $p$ , so $p ∣ r_{i} \sum \frac{1}{( p - 1 ) ^{2}} \leq 4 n > D_{0} \sum \frac{1}{n ^{2}} \leq \frac{4}{⌊ D _{0} ⌋} \leq \frac{8}{D _{0}},$ using the integral comparison $\sum_{n > M} n^{- 2} \leq \int_{M}^{\infty} t^{- 2} d t = 1/ M$ at the integer $M = ⌊ D_{0} ⌋$ , and $⌊ D_{0} ⌋ \geq D_{0} /2$ for $D_{0} \geq 1$ . Summing over the $k$ coordinates gives $\sum_{j} x_{j} \leq 8 k / D_{0}$ , so the lemma holds with $C := 8 k$ . ◻

Lemma 7.13 (Bound for the free-coordinate marginal). There is a constant $C = C (k) > 0$ with the following property. Let $W \geq 1$ and let $R \geq 1$ be real with $p \leq R$ for every prime $p ∣ W$ . Let $λ$ have permissible support, with $y$ -variables $y$ . Then, for every $m \in {1, \dots, k}$ and every $r \in N^{k}$ , $Y^{(m)} (r_{1}, \dots, r_{k}) \leq C \frac{y _{m a x} φ ( W ) ( lo g R + 1 )}{W} .$

Uses: Definition 7.10, Definition 4.27, Definition 3.39, Definition 3.37, Definition 3.29, Definition 3.4

Proof. Write $r^{(a)}$ for the tuple obtained from $r$ by putting $a$ in the $m$ -th slot. By Lemma 4.21, $y (r^{(a)}) = 0$ unless $\prod_{i} r_{i}^{(a)}$ is squarefree, coprime to $W$ , and at most $R$ ; in particular $a$ must lie in $S := {a \in N : a \leq R, a squarefree, (a, W) = 1} .$ Hence, by the triangle inequality and $∣ y ∣ \leq y_{m a x}$ , $Y^{(m)} (r) \leq y_{m a x} a \in S \sum \frac{1}{φ ( a )} .$ It remains to bound $A := \sum_{a \in S} 1/ φ (a)$ . For squarefree $a$ one has the divisor-sum identity $a / φ (a) = \sum_{d ∣ a} μ (d)^{2} / φ (d)$ , so $1/ φ (a) = a^{- 1} \sum_{d ∣ a} μ (d)^{2} / φ (d)$ . Writing $a = d e$ and dropping the constraints linking $d$ and $e$ (all terms being non-negative), $A \leq (d \geq 1 d squarefree, (d, W) = 1 \sum \frac{μ ( d ) ^{2}}{φ ( d ) d}) \cdot (e \leq R (e, W) = 1 \sum \frac{1}{e}) .$ The first factor is bounded by an absolute constant $K$ : extending it to all squarefree $d \geq 1$ and factoring the resulting Euler product gives $\prod_{p} (1 + 1/ (p (p - 1))) < \infty$ . The second factor is the Mertens-type coprime harmonic sum, which by Lemma 6.20 is $O ((φ (W) / W) (lo g R + 1))$ under the stated hypothesis that every prime factor of $W$ is at most $R$ . Multiplying the two bounds gives $A \leq C φ (W) (lo g R + 1) / W$ for a constant $C = C (k) > 0$ , and the lemma follows. ◻

Proof uses: Lemma 4.21, Lemma 6.20, Definition 3.3

Lemma 7.14 (Off-diagonal contribution: $a_{j} \neq = r_{j}$ for some $j \neq = m$ ). There is a constant $C = C (k) > 0$ with the following property. Let $ϑ \in (0, 1)$ and $δ \in (0, ϑ /2)$ . Then there is $N_{0}$ such that for every $N \geq N_{0}$ , every $y$ of permissible support, every $m \in {1, \dots, k}$ , and every $r \in N^{k}$ with $r_{i} \geq 1$ for every $i$ and $r_{m} = 1$ , $a \in N^{k} : r_{i} ∣ a_{i} \forall i \exists j \neq = m, a_{j} \neq = r_{j} \sum T_{m, r} (a) \leq C \frac{y _{m a x} φ ( W ) lo g R}{W D _{0}} .$

Lean: PrimeGaps.MaynardOffDiagonal.offDiagonal_bound

Uses: Definition 7.9, Definition 4.27, Definition 3.39, Definition 3.29, Definition 3.28, Definition 3.37

Proof. If $k \leq 1$ the off-diagonal index set is empty and there is nothing to prove, so assume $k \geq 2$ .

Step 1: a $y$ -free majorant. On the permissible support every coordinate $a_{i}$ is positive, squarefree and coprime to $W$ , and $\prod_{i} a_{i} \leq R$ . Since $∣ y (a) ∣ \leq y_{m a x}$ and $∣ μ ∣ \leq 1$ , Definition 7.9 gives, for every permissible $a$ , $T_{m, r} (a) \leq y_{m a x} \cdot i = 1 \prod k μ (r_{i}) g (r_{i}) \cdot \frac{1}{\prod _{i = 1}^{k} φ ( a _{i} )} \cdot i \neq = m \prod \frac{r _{i}}{φ ( a _{i} )} .$ Summing over the off-diagonal set, the whole off-diagonal sum is at most $y_{m a x} K$ , where $K$ denotes the sum of the right-hand majorant (without the factor $y_{m a x}$ ) over all permissible off-diagonal $a$ .

Step 2: reduction to one-dimensional sums. Every contributing $a$ has $r_{i} ∣ a_{i}$ ; write $a_{i} = r_{i} b_{i}$ with $b_{i} \geq 1$ . On the permissible support each $a_{i}$ is squarefree, so $(r_{i}, b_{i}) = 1$ and $φ (a_{i}) = φ (r_{i}) φ (b_{i})$ ; moreover each $b_{i}$ is itself squarefree, coprime to $W$ , and at most $R$ , that is, $b_{i} \in S$ , where $S := {n \leq R : n squarefree, (n, W) = 1}$ . In these variables the majorant factors as $=: Π (r) i \prod μ (r_{i}) g (r_{i}) \cdot \frac{1}{\prod _{i} φ ( r _{i} )} \cdot i \neq = m \prod \frac{r _{i}}{φ ( r _{i} )} \cdot \frac{1}{φ ( b _{m} )} i \neq = m \prod \frac{1}{φ ( b _{i} ) ^{2}} .$ Now $Π (r) \leq 1$ : indeed $∣ μ ∣ \leq 1$ , the $m$ -th coordinate contributes $g (1) / φ (1) = 1$ since $r_{m} = 1$ , and for each $i \neq = m$ the squarefreeness of $r_{i}$ gives $g (r_{i}) r_{i} \leq φ (r_{i})^{2}$ , this being the inequality $\prod_{p ∣ r_{i}} (1 - (p - 1)^{- 2}) \leq 1$ . Being off-diagonal means $a_{j} \neq = r_{j}$ , i.e. $b_{j} \neq = 1$ , for at least one $j \neq = m$ ; bounding the number of such $j$ by $k - 1$ and summing each coordinate independently, $K A B T \leq := := := (k - 1) A \cdot T \cdot B^{k - 2}, n \in S \sum \frac{1}{φ ( n )}, n \in S \sum \frac{1}{φ ( n ) ^{2}}, n \in S n \neq = 1 \sum \frac{1}{φ ( n ) ^{2}},$ where $A$ accounts for the free $m$ -th coordinate, $T$ for the distinguished offending coordinate $j$ , and $B$ for each of the remaining $k - 2$ coordinates.

Step 3: the three sums. First, $B \leq \sum_{n \geq 1} μ (n)^{2} / φ (n)^{2} =: C_{B}$ , which is finite by Lemma 6.11 and absolute. Second, every $n \in S$ with $n \neq = 1$ is squarefree and coprime to $W$ , hence has all of its prime factors exceeding $D_{0}$ (Definition 3.29); choosing one such prime factor $p$ and writing $n = p n^{'}$ with $n^{'} \in S$ coprime to $p$ , we have $φ (n) = (p - 1) φ (n^{'})$ , so, over-counting each $n$ at most once per prime factor, $T \leq (p > D_{0} \sum \frac{1}{( p - 1 ) ^{2}}) \cdot B \leq \frac{8}{D _{0}} \cdot C_{B},$ the bound on the prime sum being the one established in the proof of Lemma 7.12. Third, $A \leq C_{A} φ (W) (lo g R + 1) / W$ exactly as in the proof of Lemma 7.13, via Lemma 6.20.

Step 4: assembly. Combining, $K \leq (k - 1) C_{A} C_{B}^{k - 1} \cdot \frac{8}{D _{0}} \cdot \frac{φ ( W ) ( lo g R + 1 )}{W} .$ Since $R = N^{ϑ /2 - δ}$ with $ϑ /2 - δ > 0$ , we have $lo g R \geq 1$ for all $N$ beyond a threshold $N_{0}$ depending only on $ϑ$ and $δ$ ; for such $N$ , $lo g R + 1 \leq 2 lo g R$ . Multiplying by $y_{m a x}$ from Step 1 gives the assertion with $C := 16 (k - 1) C_{A} C_{B}^{k - 1}$ . ◻

Proof uses: Lemma 4.21, Lemma 7.12, Lemma 7.13, Lemma 6.20, Lemma 6.11

Lemma 7.15 ( $y^{(m)}$ from $y$ ). There is a constant $C = C (k) > 0$ with the following property. Let $ϑ \in (0, 1)$ and $δ \in (0, ϑ /2)$ . Then there is $N_{0}$ such that for every $N \geq N_{0}$ , every $λ$ of permissible support, every $m \in {1, \dots, k}$ , and every $r \in N^{k}$ with $r_{m} = 1$ and every $r_{i}$ squarefree, $y^{(m)} (r_{1}, \dots, r_{k}) - Y^{(m)} (r_{1}, \dots, r_{k}) \leq C \frac{y _{m a x} φ ( W ) lo g R}{W D _{0}} .$

Lean: PrimeGaps.maynard_ym_identity

Uses: Definition 4.25, Definition 7.10, Definition 4.27, Definition 3.39, Definition 3.29, Definition 3.28, Definition 3.37

Proof. Squarefreeness of each $r_{i}$ gives $r_{i} \geq 1$ , so Lemma 7.11 applies and, writing $c (m, r) := \prod_{i \neq = m} g (r_{i}) r_{i} / φ (r_{i})^{2}$ , $y^{(m)} (r) - Y^{(m)} (r) = (c (m, r) - 1) Y^{(m)} (r) + a : r_{i} ∣ a_{i} \forall i \exists j \neq = m, a_{j} \neq = r_{j} \sum T_{m, r} (a) .$ The second term is bounded by Lemma 7.14, applied to the $y$ -variables of $λ$ , which have permissible support by Lemma 4.21; this gives $C_{1} y_{m a x} φ (W) lo g R / (W D_{0})$ for all $N$ beyond a threshold. We bound the first term.

If some $r_{j}$ with $j \neq = m$ is not coprime to $W$ , then every tuple obtained from $r$ by varying the $m$ -th coordinate has coordinate product not coprime to $W$ , so $y$ vanishes at all of them by Lemma 4.21; hence $Y^{(m)} (r) = 0$ and the first term vanishes.

Otherwise every $r_{i}$ is squarefree and coprime to $W$ , so by Definition 3.29 every prime factor of every $r_{i}$ exceeds $D_{0}$ . Applying Lemma 7.12 to the tuple $r$ — whose $m$ -th factor equals $1$ , so that the full product and the product over $i \neq = m$ agree — gives $∣ c (m, r) - 1∣ \leq C_{2} / D_{0}$ once $D_{0} \geq 2$ , which holds for all large $N$ . Combined with Lemma 7.13, $(c (m, r) - 1) Y^{(m)} (r) \leq \frac{C _{2}}{D _{0}} \cdot C_{3} \frac{y _{m a x} φ ( W ) ( lo g R + 1 )}{W} \leq 2 C_{2} C_{3} \frac{y _{m a x} φ ( W ) lo g R}{W D _{0}},$ using $lo g R + 1 \leq 2 lo g R$ , valid for all $N$ beyond a threshold depending only on $ϑ$ and $δ$ . Adding the two contributions, and taking $N_{0}$ to be the largest of the finitely many thresholds used, gives the claim with $C := C_{1} + 2 C_{2} C_{3}$ . ◻

Proof uses: Lemma 7.11, Lemma 7.14, Lemma 7.12, Lemma 7.13, Lemma 4.21, Definition 7.9, Definition 3.6

7.5 The smooth case

Lemma 7.16 (Substitute smooth $y$ into Lemma 7.15). There is a constant $C = C (k) \geq 0$ with the following property. Let $ϑ \in (0, 1)$ , $δ \in (0, ϑ /2)$ , and let $F : R^{k} \to R$ be smooth with $supp F \subseteq R_{k}$ . Then there is $N_{0}$ such that for every $N \geq N_{0}$ , every $λ$ of permissible support whose $y$ -variables satisfy $y_{m a x} \leq F_{m a x}$ , every $m \in {1, \dots, k}$ , and every $r \in N^{k}$ with $r_{m} = 1$ and every $r_{i}$ squarefree, $y^{(m)} (r_{1}, \dots, r_{k}) - Y^{(m)} (r_{1}, \dots, r_{k}) \leq C \frac{F _{m a x} φ ( W ) lo g R}{W D _{0}} .$

Lean: MaynardSmoothY.exists_abs_ym_sub_yInverseSum_le

Uses: Lemma 7.15, Definition 7.4, Definition 4.25, Definition 7.10, Definition 4.27, Definition 5.1, Definition 3.39, Definition 3.29, Definition 3.28, Definition 3.37

Proof. Apply Lemma 7.15, which bounds the left-hand side by $C y_{m a x} φ (W) lo g R / (W D_{0})$ for all $N$ beyond a threshold. For all such $N$ we have $lo g R > 0$ , and $φ (W) / W > 0$ always, so that bound is a non-decreasing function of $y_{m a x}$ . Replacing $y_{m a x}$ by the larger quantity $F_{m a x}$ using the hypothesis $y_{m a x} \leq F_{m a x}$ yields the stated bound with the same constant. ◻

Lemma 7.17 (Maximal modulus of the transformed coefficients). Let $k \geq 1$ , let $R \geq 2$ , and let $y : N^{k} \to R$ be finitely supported with permissible support at level $R$ and modulus $W$ (Definition 3.39). Then the transformed system $λ_{y}$ of Definition 4.22 satisfies $∥ λ_{y} ∥_{m a x} \leq e^{1 + 3 k} ∥ y ∥_{m a x} (lo g R)^{k} .$

Lean: PrimeGaps.max_yToL_le_const_mul_max_y_mul_log_pow

Uses: Definition 4.22, Definition 4.27, Definition 3.39

Proof. Fix $d$ . Expanding $λ_{y} (d)$ and bounding each summand by $∥ y ∥_{m a x}$ leaves the divisor sum $\sum_{r} \prod_{i} μ (r_{i})^{2} / φ (r_{i})$ taken over those $r$ with $d_{i} ∣ r_{i}$ and $\prod_{i} r_{i} \leq R$ . Together with the prefactor $\prod_{i} μ (d_{i}) d_{i}$ this is exactly the quantity bounded in Lemma 6.10, taken at modulus $W$ and at the present $d$ . Each coordinate factor is at most $\sum_{r \leq R} μ (r)^{2} / φ (r) \leq e (1 + lo g R)$ , and the outer product over the $k$ coordinates contributes at most $e^{3 k}$ after absorbing the prefactor $\prod_{i} μ (d_{i}) d_{i}$ against the coprimality constraints. Multiplying the $k$ coordinate bounds and using $1 + lo g R \leq e lo g R$ for $R \geq 2$ gives the stated bound. ◻

Proof uses: Lemma 6.10

8 Sieve manipulations: the reduction of $S_{1} (λ)$

For the first moment $S_{1} (λ)$ , we pass from the coefficients $λ (d_{1}, \dots, d_{k})$ to the $y$ -variables. We expand the square defining $w_{n}$ and interchange the order of summation (Lemma 8.6); we evaluate the resulting inner count by the Chinese remainder theorem and bound the aggregate error (Lemmas 8.7–8.10); we split $1/ [d_{i}, e_{i}]$ across the two coordinates, detect the residual cross-coprimality by Möbius inversion, and restrict the resulting off-diagonal variables (Lemmas 8.11–8.15); we substitute the inversion formula expressing $λ$ in terms of $y$ , and show that all but the diagonal term $s_{i, j} \equiv 1$ is negligible (Lemmas 8.16–8.21); and finally we insert the $F$ -derived weight, drop the last coprimality constraint, and convert the discrete sum to an integral by partial summation (Lemmas 8.22–8.25). The final statement, Lemma 8.25, is the asymptotic $S_{1} (λ_{0}) = \frac{φ ( W ) ^{k} N ( lo g R ) ^{k}}{W ^{k + 1}} I_{k} (F) + O_{k} (\frac{F _{m a x}^{2} φ ( W ) ^{k} N ( lo g R ) ^{k}}{W ^{k + 1} D _{0}}) .$

Throughout, $k \geq 2$ is fixed, $H = {h_{1}, \dots, h_{k}}$ is admissible (Definition 3.15), $ϑ \in (0, 1)$ and $δ \in (0, ϑ /2)$ are fixed real parameters, $R = N^{ϑ /2 - δ}$ (Definition 3.37), $D_{0} = lo g lo g lo g N$ (Definition 3.28), $W = \prod_{p \leq D_{0}} p$ (Definition 3.29), and $v_{0}$ is a valid residue class (Lemma 3.34). No level-of-distribution hypothesis is used in this section: $ϑ$ enters only through the truncation $R$ , and the arithmetic input is elementary (Mertens sums and partial summation). Bombieri–Vinogradov is needed only for the second moment.

8.1 Auxiliary objects

Definition 8.1 (The lcm modulus $q (d, e)$ ). Let $d = (d_{1}, \dots, d_{k})$ and $e = (e_{1}, \dots, e_{k})$ be $k$ -tuples of positive integers. Define $q (d, e) := W i = 1 \prod k [d_{i}, e_{i}] .$

Lean: PrimeGaps.qMod

Uses: Definition 3.29, Notation 4.11

Definition 8.2 (The CRT remainder $ϱ (d, e)$ ). For $k$ -tuples $d, e$ of positive integers, set $ϱ (d, e) := N < n \leq 2 N n \equiv v_{0} (mod W) [d_{i}, e_{i}] ∣ n + h_{i} \forall i \sum 1 - \frac{N}{q ( d , e )} 1 [W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}] are pairwise coprime] .$

Uses: Definition 8.1, Definition 3.29, Notation 4.11

Notation 8.3 (Restricted sum $\sum^{*}$ over the $s_{i, j}$ ). Fix positive integers $u_{1}, \dots, u_{k}$ . For a function $f$ of the variables $(s_{i, j})_{1 \leq i \neq = j \leq k}$ we write $s_{1, 2}, \dots, s_{k, k - 1} \sum * f ((s_{i, j})_{i \neq = j}) := s_{i, j} \geq 1, 1 \leq i \neq = j \leq k (*_{1}), (*_{2}), (*_{3}), (*_{4}) \sum f ((s_{i, j})_{i \neq = j}),$ where the four restrictions are $(*_{1}) (*_{2}) (*_{3}) (*_{4}) (s_{i, j}, u_{i}) = 1 (s_{i, j}, u_{j}) = 1 (s_{i, j}, s_{i, a}) = 1 (s_{i, j}, s_{b, j}) = 1 for all i \neq = j, for all i \neq = j, for all a \in / {i, j}, for all b \in / {i, j} .$

Lean: PrimeGaps.LemS1RestrictSij.SigmaRestr

Definition 8.4 (The exponent tuple $a$ ). Given positive integers $u_{1}, \dots, u_{k}$ and $(s_{i, j})_{1 \leq i \neq = j \leq k}$ , set $a_{j} a := := u_{j} i \neq = j \prod s_{j, i} (1 \leq j \leq k), (a_{1}, \dots, a_{k}) .$

Lean: PrimeGaps.boldA

Definition 8.5 (The exponent tuple $b$ ). With the same data, set $b_{j} b := := u_{j} i \neq = j \prod s_{i, j} (1 \leq j \leq k), (b_{1}, \dots, b_{k}) .$ Note the transposition of the indices of $s$ relative to Definition 8.4: in $a_{j}$ the first index of $s$ is fixed to $j$ , in $b_{j}$ the second.

Lean: PrimeGaps.boldB

Uses: Definition 8.4

8.2 Expansion and the Chinese remainder theorem

Lemma 8.6 (Expansion of $S_{1} (λ)$ ). Let $λ : N^{k} \to R$ have finite support. Then $S_{1} (λ) = d \sum e \sum λ (d) λ (e) N < n \leq 2 N n \equiv v_{0} (mod W) [d_{i}, e_{i}] ∣ n + h_{i} \forall i \sum 1.$

Lean: PrimeGaps.lem_S1_expansion_S1_expansion

Uses: Definition 4.14, Definition 4.12, Definition 3.29, Notation 4.11, Notation 3.35

Proof. We perform three rearrangements.

Step 1: expand the square. By Definition 4.12, $w_{n} = (d_{i} ∣ n + h_{i} \forall i \sum λ (d))^{2} = d_{i} ∣ n + h_{i} \forall i \sum e_{i} ∣ n + h_{i} \forall i \sum λ (d) λ (e),$ the second equality being the distributive law for the product of two finite sums (both inner sums are over divisors of the fixed positive integers $n + h_{i}$ , hence finite).

Step 2: substitute into $S_{1}$ . By Definition 4.14, $S_{1} (λ) = N < n \leq 2 N n \equiv v_{0} (mod W) \sum d_{i} ∣ n + h_{i} \forall i \sum e_{i} ∣ n + h_{i} \forall i \sum λ (d) λ (e) .$

Step 3: interchange. All three sums are finite: the outer one is over a finite arithmetic progression in $(N, 2 N]$ , and the inner ones are supported in the finite support of $λ$ . Interchanging, and merging the two divisibilities $d_{i} ∣ n + h_{i}$ and $e_{i} ∣ n + h_{i}$ into the single condition $[d_{i}, e_{i}] ∣ n + h_{i}$ , gives the assertion. ◻

Lemma 8.7 (CRT evaluation of the inner count). Let $λ$ have $R$ -permissible support (Definition 3.39), let $v_{0}$ be a valid residue class, and let $d, e$ be $k$ -tuples of positive integers with $λ (d) \neq = 0$ and $λ (e) \neq = 0$ . If $N$ is large enough that $∣ h_{i} - h_{j} ∣ \leq D_{0}$ for all $i \neq = j$ , then $N < n \leq 2 N n \equiv v_{0} (mod W) [d_{i}, e_{i}] ∣ n + h_{i} \forall i \sum 1 = ⎩ ⎨ ⎧ \frac{N}{q ( d , e )} + O (1) 0 if W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}] are pairwise coprime, otherwise,$ with an absolute implied constant.

Lean: PrimeGaps.lem_S1_CRT

Uses: Definition 3.39, Definition 3.29, Definition 3.28, Definition 8.1, Lemma 3.34, Notation 4.11, Notation 3.35

Proof. Write $q := q (d, e)$ . The summation imposes the system of congruences $n \equiv v_{0} (mod W)$ and $n \equiv - h_{i} (mod [d_{i}, e_{i}])$ for $i = 1, \dots, k$ .

Coprime case. If the $k + 1$ moduli $W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}]$ are pairwise coprime, the Chinese remainder theorem gives a unique solution modulo their product, which is exactly $q$ . The interval $(N, 2 N]$ has length $N$ , so it contains $N / q + O (1)$ integers in a fixed residue class modulo $q$ ; the error is at most $1$ in absolute value.

Non-coprime case. Suppose the moduli are not pairwise coprime, so some prime $p$ divides two of them. If $p ∣ W$ and $p ∣ [d_{i}, e_{i}]$ for some $i$ , then $p \leq D_{0}$ by Definition 3.29, while $[d_{i}, e_{i}]$ divides $\prod_{ℓ} d_{ℓ} e_{ℓ}$ , which is coprime to $W$ by $R$ -permissibility of the support (Definition 3.39); this is a contradiction, so this case does not occur. Otherwise $p ∣ [d_{i}, e_{i}]$ and $p ∣ [d_{j}, e_{j}]$ for some $i \neq = j$ . Any $n$ counted by the sum satisfies $p ∣ n + h_{i}$ and $p ∣ n + h_{j}$ , hence $p ∣ h_{i} - h_{j}$ . As $p ∤ W$ we have $p > D_{0}$ , whereas $0 < ∣ h_{i} - h_{j} ∣ \leq D_{0}$ for $N$ large; so $h_{i} - h_{j}$ is a nonzero integer of absolute value smaller than $p$ , and $p ∣ h_{i} - h_{j}$ is impossible. The set of counted $n$ is therefore empty and the sum is $0$ . ◻

Lemma 8.8 (Aggregate CRT lookup error). Let $δ \in (0, ϑ /2)$ and let $λ$ have $R$ -permissible support. Then, for all sufficiently large $N$ , with $ϱ$ as in Definition 8.2, $d \sum e \sum λ (d) λ (e) ϱ (d, e) \leq λ_{m a x}^{2} d \sum e \sum ∣ ϱ (d, e) ∣ ≪_{k} λ_{m a x}^{2} R^{2} (lo g R)^{2 k} ≪_{k} y_{m a x}^{2} R^{2} (lo g R)^{4 k},$ the sums being over the (finite) support of $λ$ .

Lean: PrimeGaps.gpy_aggregate_remainder_bound

Uses: Definition 3.39, Definition 3.37, Definition 8.2, Definition 4.20, Definition 4.27, Lemma 8.7, Notation 4.11

Proof. The first inequality is the triangle inequality together with $∣ λ (d) λ (e) ∣ \leq λ_{m a x}^{2}$ .

Step 1: each remainder is bounded. By Lemma 8.7, for every pair $(d, e)$ in the support of $λ$ we have $∣ ϱ (d, e) ∣ \leq C_{ϱ}$ for an absolute constant $C_{ϱ}$ : in the pairwise coprime case $ϱ$ is the $O (1)$ discrepancy of the count, and in the remaining case both terms defining $ϱ$ vanish.

Step 2: count the tuples in the support. By $R$ -permissibility every $d$ in the support satisfies $d_{i} \geq 1$ for all $i$ and $\prod_{i} d_{i} \leq R$ . The number of such tuples is at most $# {d \in N^{k} : i \prod d_{i} \leq R} \leq ⌊ R ⌋ \cdot (1 \leq a \leq ⌊ R ⌋ \sum \frac{1}{a})^{k} ≪_{k} R (lo g R)^{k} .$ The middle bound holds because on the counting set one has $1 \leq R \prod_{i} d_{i}^{- 1}$ , so the cardinality is at most $R \sum_{d} \prod_{i} d_{i}^{- 1}$ with each $d_{i}$ running over $[1, ⌊ R ⌋]$ , and this factorises into $k$ harmonic sums; the last step uses $\sum_{a \leq x} 1/ a \leq 1 + lo g x$ .

Step 3: assemble. Squaring Step 2 bounds the number of pairs by $≪_{k} R^{2} (lo g R)^{2 k}$ ; multiplying by $C_{ϱ} λ_{m a x}^{2}$ gives the second inequality.

Step 4: pass from $λ_{m a x}$ to $y_{m a x}$ . By Lemma 7.17, $λ_{m a x} ≪_{k} y_{m a x} (lo g R)^{k}$ , so $λ_{m a x}^{2} ≪_{k} y_{m a x}^{2} (lo g R)^{2 k}$ ; substituting gives the last bound. ◻

Proof uses: Lemma 7.17

Lemma 8.9 (Negligibility of the CRT lookup error). Let $ϑ \in (0, 1)$ , $δ \in (0, ϑ /2)$ and $Y \geq 0$ . Then, for all sufficiently large $N$ , $Y^{2} R^{2} (lo g R)^{4 k} ≪_{k} \frac{Y ^{2} φ ( W ) ^{k} N ( lo g R ) ^{k}}{W ^{k + 1} D _{0}} .$

Lean: PrimeGaps.crt_error_negligible

Uses: Definition 3.37, Definition 3.28, Definition 3.29, Definition 3.4

Proof. Both sides carry the factor $Y^{2} \geq 0$ , so we may divide it out.

Step 1: polynomial saving. By Definition 3.37, $R^{2} = N^{ϑ - 2 δ}$ , and $ϑ - 2 δ < ϑ < 1$ . Put $η := 1 - (ϑ - 2 δ) > 0$ , so $R^{2} = N^{1 - η}$ and, using $lo g R \leq lo g N$ , $R^{2} (lo g R)^{4 k} \leq N^{1 - η} (lo g N)^{4 k} .$

Step 2: the $W$ -factor is harmless. By Lemma 3.32, $W ≪ (lo g lo g N)^{2} \leq lo g N$ for large $N$ , so $W^{k + 1} \leq (lo g N)^{2 k + 2}$ ; combined with $φ (W) \geq 1$ this gives $φ (W)^{k} (lo g N)^{2 k + 2} / W^{k + 1} \geq 1$ .

Step 3: combine. Multiplying the bound of Step 1 by the quantity of Step 2, $R^{2} (lo g R)^{4 k} \leq N^{1 - η} (lo g N)^{6 k + 2} \frac{φ ( W ) ^{k}}{W ^{k + 1}} = N \frac{φ ( W ) ^{k}}{W ^{k + 1}} \cdot N^{- η} (lo g N)^{6 k + 2} .$ Since $lo g R = (ϑ /2 - δ) lo g N$ and $D_{0} = lo g lo g lo g N$ , the target factor $(lo g R)^{k} / D_{0}$ is $≫_{k} (lo g N)^{k} / lo g lo g lo g N$ , whereas $N^{- η} (lo g N)^{6 k + 2} \to 0$ as $N \to \infty$ because $η > 0$ dominates any fixed power of $lo g N$ . Hence $N^{- η} (lo g N)^{6 k + 2} \leq (lo g R)^{k} / D_{0}$ for large $N$ , which is the claim. ◻

Proof uses: Lemma 3.32

Lemma 8.10 (Main term of $S_{1} (λ)$ after the CRT step). Let $k \geq 2$ , let $H$ be admissible, let $ϑ \in (0, 1)$ and $δ \in (0, ϑ /2)$ . Then, for all sufficiently large $N$ , for every $λ$ with $R$ -permissible support and every valid $v_{0}$ , $S_{1} (λ) = \frac{N}{W} d, e \sum' \frac{λ ( d ) λ ( e )}{\prod _{i = 1}^{k} [ d _{i} , e _{i} ]} + O_{k} (\frac{y _{m a x}^{2} φ ( W ) ^{k} N ( lo g R ) ^{k}}{W ^{k + 1} D _{0}}),$ where $\sum^{'}$ denotes summation restricted to pairs $(d, e)$ of tuples of positive integers for which $W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}]$ are pairwise coprime.

Lean: GPYSieveS1.main_S1_asymptotic

Uses: Definition 4.14, Definition 3.15, Definition 3.39, Definition 3.37, Definition 3.28, Definition 3.29, Definition 4.20, Definition 4.27, Lemma 3.34, Notation 4.11, Notation 3.35

Proof. Step 1. By Lemma 8.6, $S_{1} (λ) = \sum_{d, e} λ (d) λ (e) T (d, e)$ , where $T (d, e)$ is the inner count.

Step 2. Admissibility makes $h_{1}, \dots, h_{k}$ distinct, so for $N$ large enough $∣ h_{i} - h_{j} ∣ \leq D_{0}$ for all $i \neq = j$ , and Lemma 8.7 applies to every pair in the support. By Definition 8.2 this says precisely $T (d, e) = \frac{N}{q ( d , e )} 1 [W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}] pairwise coprime] + ϱ (d, e) .$ Substituting into Step 1 and using $N / q (d, e) = (N / W) \prod_{i} [d_{i}, e_{i}]^{- 1}$ , $S_{1} (λ) = \frac{N}{W} d, e \sum' \frac{λ ( d ) λ ( e )}{\prod _{i} [ d _{i} , e _{i} ]} + d, e \sum λ (d) λ (e) ϱ (d, e) .$

Step 3. By Lemma 8.8 the second sum is $≪_{k} y_{m a x}^{2} R^{2} (lo g R)^{4 k}$ .

Step 4. By Lemma 8.9 applied with $Y = y_{m a x}$ , this is $≪_{k} y_{m a x}^{2} φ (W)^{k} N (lo g R)^{k} / (W^{k + 1} D_{0})$ , which is the stated error term. ◻

Proof uses: Lemma 8.6, Lemma 8.7, Lemma 8.8, Lemma 8.9, Definition 8.2, Definition 8.1

8.3 Decoupling the lcm and the Möbius inversion

Lemma 8.11 (Removing the automatic constraints). Let $λ : N^{k} \to R$ be such that $λ (t) \neq = 0$ implies that every $t_{i}$ is positive, $\prod_{i} t_{i}$ is squarefree, and $(\prod_{i} t_{i}, W) = 1$ . Then, for every function $f$ of pairs of tuples, $d, e \sum' λ (d) λ (e) f (d, e) = d, e (d_{i}, e_{j}) = 1 \forall i \neq = j \sum λ (d) λ (e) f (d, e),$ where $\sum^{'}$ is the restricted summation of Lemma 8.10.

Lean: PrimeGaps.lem_S1_remove_automatic

Uses: Lemma 8.10, Definition 3.39, Definition 3.29, Notation 4.11

Proof. It suffices to show that, on the support of $λ (d) λ (e)$ , the pairwise coprimality of $W, [d_{1}, e_{1}], \dots, [d_{k}, e_{k}]$ is equivalent to $(d_{i}, e_{j}) = 1$ for all $i \neq = j$ ; both sides then have the same summands.

Step 1: the intra-coprimalities are automatic. If $λ (d) \neq = 0$ then $\prod_{i} d_{i}$ is squarefree. If a prime $p$ divided both $d_{i}$ and $d_{j}$ with $i \neq = j$ , then $p^{2} ∣ \prod_{ℓ} d_{ℓ}$ , a contradiction. Hence $(d_{i}, d_{j}) = 1$ for $i \neq = j$ , and likewise $(e_{i}, e_{j}) = 1$ for $i \neq = j$ .

Step 2: coprimality to $W$ is automatic. From $(\prod_{i} d_{i}, W) = 1$ and $(\prod_{i} e_{i}, W) = 1$ , and since $[d_{i}, e_{i}]$ divides $\prod_{ℓ} d_{ℓ} e_{ℓ}$ , we get $([d_{i}, e_{i}], W) = 1$ for every $i$ .

Step 3: the residual condition. Pairwise coprimality of the $k + 1$ moduli unwinds into $([d_{i}, e_{i}], W) = 1$ for all $i$ (Step 2) together with $([d_{i}, e_{i}], [d_{j}, e_{j}]) = 1$ for $i \neq = j$ . A prime $p$ dividing both $[d_{i}, e_{i}]$ and $[d_{j}, e_{j}]$ divides one of $d_{i}, e_{i}$ and one of $d_{j}, e_{j}$ ; by Step 1 the possibilities $p ∣ d_{i}, d_{j}$ and $p ∣ e_{i}, e_{j}$ are excluded, leaving $p ∣ (d_{i}, e_{j})$ or $p ∣ (d_{j}, e_{i})$ . Thus the only non-automatic constraint is $(d_{i}, e_{j}) = 1$ for all $i \neq = j$ , and conversely that constraint together with Steps 1–2 gives the full pairwise coprimality. ◻

Lemma 8.12 (Decoupling the outer lcm product). Let $λ : N^{k} \to R$ be such that $λ (t) \neq = 0$ implies that every $t_{i}$ is positive and squarefree and that $t_{1}, \dots, t_{k}$ are pairwise coprime. Then $d, e (d_{i}, e_{j}) = 1 \forall i \neq = j \sum \frac{λ ( d ) λ ( e )}{\prod _{i = 1}^{k} [ d _{i} , e _{i} ]} = d, e (d_{i}, e_{j}) = 1 \forall i \neq = j \sum (u_{1}, \dots, u_{k} u_{i} ∣ (d_{i}, e_{i}) \forall i \sum i = 1 \prod k φ (u_{i})) \frac{λ ( d ) λ ( e )}{\prod _{i = 1}^{k} d _{i} e _{i}} .$

Lean: PrimeGaps.lem_S1_decouple_lcm

Uses: Lemma 8.11, Lemma 6.3, Definition 3.4, Notation 4.11

Proof. We may work summand by summand, and we may assume $λ (d) λ (e) \neq = 0$ , since otherwise both summands vanish. Then every $d_{i}$ and every $e_{i}$ is positive and squarefree, so Lemma 6.3 gives, for each $i$ , $\frac{1}{[ d _{i} , e _{i} ]} = \frac{1}{d _{i} e _{i}} u_{i} ∣ (d_{i}, e_{i}) \sum φ (u_{i}) .$ Taking the product over $i = 1, \dots, k$ and expanding the product of $k$ finite sums into a single sum over the tuple $(u_{1}, \dots, u_{k})$ with $u_{i} ∣ (d_{i}, e_{i})$ , $\frac{1}{\prod _{i = 1}^{k} [ d _{i} , e _{i} ]} = \frac{1}{\prod _{i = 1}^{k} d _{i} e _{i}} u_{1}, \dots, u_{k} u_{i} ∣ (d_{i}, e_{i}) \forall i \sum i = 1 \prod k φ (u_{i}) .$ Multiplying by $λ (d) λ (e)$ and summing over the pairs satisfying the cross-coprimality guard gives the identity; the guard is a condition on $(d, e)$ alone and is untouched by the manipulation, since the $u$ -sum is internal to the summand. ◻

Lemma 8.13 (Möbius inversion of the constraint $(d_{i}, e_{j}) = 1$ ). For every finite family of coefficients $λ$ and every pair $(d, e)$ , $d, e (d_{i}, e_{j}) = 1 \forall i \neq = j \sum (u_{1}, \dots, u_{k} u_{i} ∣ (d_{i}, e_{i}) \sum i \prod φ (u_{i})) \frac{λ ( d ) λ ( e )}{\prod _{i} d _{i} e _{i}} = Σ_{full},$ where $Σ_{full}$ is the finite sum $Σ_{full} = d, e \sum u_{1}, \dots, u_{k} u_{i} ∣ (d_{i}, e_{i}) \sum s_{1, 2}, \dots, s_{k, k - 1} s_{i, j} ∣ (d_{i}, e_{j}) (i \neq = j) \sum (i = 1 \prod k φ (u_{i})) (i \neq = j \prod μ (s_{i, j})) \frac{λ ( d ) λ ( e )}{\prod _{i = 1}^{k} d _{i} e _{i}} .$

Lean: PrimeGaps.LemS1RestrictSij.lem_S1_mobius_coprime

Uses: Lemma 8.12, Definition 3.3, Definition 3.4, Notation 4.11

Proof. Step 1: factor the indicator. The constraint is a conjunction over the $k (k - 1)$ ordered pairs $(i, j)$ with $i \neq = j$ , so $1 [(d_{i}, e_{j}) = 1 \forall i \neq = j] = i \neq = j \prod 1 [(d_{i}, e_{j}) = 1] .$

Step 2: detect each factor by Möbius inversion. By Lemma 3.7 applied at $n = (d_{i}, e_{j})$ , $1 [(d_{i}, e_{j}) = 1] = s_{i, j} ∣ (d_{i}, e_{j}) \sum μ (s_{i, j}),$ and $s_{i, j} ∣ (d_{i}, e_{j})$ is the conjunction $s_{i, j} ∣ d_{i}$ and $s_{i, j} ∣ e_{j}$ . Taking the product over the $k (k - 1)$ pairs turns Step 1 into a single sum over tuples $(s_{i, j})_{i \neq = j}$ of positive integers weighted by $\prod_{i \neq = j} μ (s_{i, j})$ .

Step 3: insert and interchange. Insert the expansion of Step 2 into the left-hand side. All sums are finite: $d, e$ range over the finite support of $λ$ , the $u_{i}$ over divisors of $(d_{i}, e_{i})$ and the $s_{i, j}$ over divisors of $(d_{i}, e_{j})$ . Interchanging the order of summation and merging the divisibility indicators into the summation ranges yields exactly $Σ_{full}$ . ◻

Proof uses: Lemma 3.7

Lemma 8.14 (Pointwise coprimalities of the $s_{i, j}$ ). Let $λ$ be such that $λ (t) \neq = 0$ implies that every $t_{i}$ is positive and that $t_{1}, \dots, t_{k}$ are pairwise coprime. Let $(d, e, u, (s_{i, j})_{i \neq = j})$ be a configuration occurring in $Σ_{full}$ , so that $u_{i} ∣ d_{i}$ , $u_{i} ∣ e_{i}$ and $s_{i, j} ∣ d_{i}$ , $s_{i, j} ∣ e_{j}$ for $i \neq = j$ , and suppose its summand is nonzero, i.e. $λ (d) λ (e) \neq = 0$ . Then the four restrictions $(*_{1})$ – $(*_{4})$ of Notation 8.3 hold.

Lean: PrimeGaps.LemS1RestrictSij.lem_S1_sij_coprimality

Uses: Lemma 8.13, Notation 8.3, Definition 3.39, Notation 4.11

Proof. By hypothesis the coordinates of $d$ are pairwise coprime and so are those of $e$ : $(d_{i}, d_{j}) = 1, (e_{i}, e_{j}) = 1 (i \neq = j) . (*)$ Each of the four cases assumes a prime $p$ divides $s_{i, j}$ and one further listed factor, and contradicts $(*)$ .

$(*_{1})$ . If $p ∣ s_{i, j}$ and $p ∣ u_{i}$ , then $p ∣ s_{i, j} ∣ e_{j}$ and $p ∣ u_{i} ∣ e_{i}$ , so $p ∣ (e_{i}, e_{j})$ with $i \neq = j$ : contradiction.

$(*_{2})$ . If $p ∣ s_{i, j}$ and $p ∣ u_{j}$ , then $p ∣ s_{i, j} ∣ d_{i}$ and $p ∣ u_{j} ∣ d_{j}$ , so $p ∣ (d_{i}, d_{j})$ : contradiction.

$(*_{3})$ . If $p ∣ s_{i, j}$ and $p ∣ s_{i, a}$ with $a \in / {i, j}$ , then $p ∣ e_{j}$ and $p ∣ e_{a}$ with $j \neq = a$ : contradiction.

$(*_{4})$ . If $p ∣ s_{i, j}$ and $p ∣ s_{b, j}$ with $b \in / {i, j}$ , then $p ∣ d_{i}$ and $p ∣ d_{b}$ with $i \neq = b$ : contradiction. ◻

Lemma 8.15 (The restricted and unrestricted $s$ -sums agree). Under the hypothesis of Lemma 8.14 on $λ$ , let $Σ_{restr}$ denote the sum obtained from $Σ_{full}$ by replacing the unrestricted $s$ -summation by the restricted summation $\sum^{*}$ of Notation 8.3. Then $Σ_{restr} = Σ_{full} .$

Lean: PrimeGaps.LemS1RestrictSij.lem_S1_restrict_sij

Uses: Lemma 8.13, Lemma 8.14, Notation 8.3, Notation 4.11

Proof. The restricted sum is obtained from the unrestricted one by deleting the configurations that violate at least one of $(*_{1})$ – $(*_{4})$ . By Lemma 8.14, every configuration whose summand is nonzero satisfies all four restrictions; contrapositively, every deleted configuration has summand $0$ . Deleting terms that vanish does not change the value of a sum, so the two sums are equal. ◻

8.4 The substitution $λ ⇝ y$

Lemma 8.16 (Substituting $y$ into $S_{1} (λ)$ ). Let $k \geq 2$ , let $H$ be admissible, let $ϑ \in (0, 1)$ and $δ \in (0, ϑ /2)$ . Then, for all sufficiently large $N$ , for every $λ$ with $R$ -permissible support and every valid $v_{0}$ , $S_{1} (λ) = \frac{N}{W} Σ_{y} (λ) + O_{k} (\frac{y _{m a x}^{2} φ ( W ) ^{k} N ( lo g R ) ^{k}}{W ^{k + 1} D _{0}}),$ where, with $a, b$ as in Definitions 8.4 and 8.5, $Σ_{y} (λ)$ is the finite sum $Σ_{y} (λ) = u \sum (i = 1 \prod k \frac{μ ( u}{φ ( u _{i} )}$

1 Introduction

2 Overview

2.1 The GPY method and the sum S2​(λ)−ρS1​(λ)

2.2 The sieve weights and the W-trick

2.3 The variational problem

3 Definitions and preliminaries

3.1 Arithmetic functions and standard notation

3.2 Admissible sets

3.3 Prime counting and the level of distribution

3.4 External analytic inputs

3.5 Prime counts in a dyadic interval

3.6 The W-trick

3.7 The truncation parameter R and the sieve support

4 The sieve datum, the sieve weights, and the auxiliary y-variables

4.1 The sieve datum

4.2 Tensor sieve coefficients

4.3 The sieve weights and the sums S1​(λ), S2​(λ)

4.4 The auxiliary y-variables

5 The variational problem

5.1 The simplex and the profile

5.2 The functionals Ik​, Jk,ε(m)​ and the constant Mk,ε​

5.3 From a profile to the sieve coefficients

5.4 Basic properties of Ik​, Jk,ε(m)​ and Mk,ε​

5.5 Smooth profiles and the variational criterion

5.6 Integration formulas on the simplex

6 Auxiliary arithmetic estimates

6.1 Elementary totient and Möbius identities

6.2 Divisor sums, Mertens-type bounds and convergent series

6.3 The constants A(M) and B(M)

6.4 Coprime harmonic and coprime-density sums

6.5 The sum Td​ and the Mertens sum over integers coprime to W

6.6 The two sieve densities

6.7 The convolution defect and the asymptotic for H

6.8 Partial summation

7 Relating the transformed weight systems

7.1 Finiteness of the marginal supremum

7.2 The y-variables of the F-derived weight

7.3 Expressing y(m) through y

7.4 The diagonal decomposition of y(m)

7.5 The smooth case

8 Sieve manipulations: the reduction of S1​(λ)

8.1 Auxiliary objects

8.2 Expansion and the Chinese remainder theorem

8.3 Decoupling the lcm and the Möbius inversion

8.4 The substitution λ⇝y

2.1 The GPY method and the sum $S_{2} (λ) - ρ S_{1} (λ)$

2.2 The sieve weights and the $W$ -trick

3.6 The $W$ -trick

3.7 The truncation parameter $R$ and the sieve support

4 The sieve datum, the sieve weights, and the auxiliary $y$ -variables

4.3 The sieve weights and the sums $S_{1} (λ)$ , $S_{2} (λ)$

4.4 The auxiliary $y$ -variables

5.2 The functionals $I_{k}$ , $J_{k, ε}^{(m)}$ and the constant $M_{k, ε}$

5.4 Basic properties of $I_{k}$ , $J_{k, ε}^{(m)}$ and $M_{k, ε}$

6.3 The constants $A (M)$ and $B (M)$

6.5 The sum $T_{d}$ and the Mertens sum over integers coprime to $W$

6.7 The convolution defect and the asymptotic for $H$

7.2 The $y$ -variables of the $F$ -derived weight

7.3 Expressing $y^{(m)}$ through $y$

7.4 The diagonal decomposition of $y^{(m)}$

8 Sieve manipulations: the reduction of $S_{1} (λ)$

8.4 The substitution $λ ⇝ y$