Improved Long Gaps Between Primes

We prove that, for all sufficiently large X, G(X) >> log(X) * log(log(X))^2 * log(log(log(log(X)))) / log(log(log(X)))^2, where G(X) is the largest gap between consecutive primes not exceeding X. Here, log denotes the natural logarithm and >> denotes a lower bound up to a positive multiplicative constant independent of X.

The main results are short_translates (Proposition 1.2) and long_gap_theorem (Theorem 1.1). The proof uses weak Mertens estimates, κ = 1/8, and a larger fixed constant in the auxiliary smoothness cutoff.

noncomputable def LongGapsBetweenPrimes.iteratedLog (j : ℕ) (x : ℝ) : ℝ

The j-fold natural logarithm used in the statement of Theorem 1.1.

Equations

• LongGapsBetweenPrimes.iteratedLog j x = Real.log^[j] x

noncomputable def LongGapsBetweenPrimes.gapScale (x : ℝ) : ℝ

The function on the right hand side of Theorem 1.1, without its constant.

Equations

• LongGapsBetweenPrimes.gapScale x = Real.log x * LongGapsBetweenPrimes.iteratedLog 2 x ^ 2 * LongGapsBetweenPrimes.iteratedLog 4 x / LongGapsBetweenPrimes.iteratedLog 3 x ^ 2

def LongGapsBetweenPrimes.ConsecutivePrimes (p q : ℕ) : Prop

Consecutive primes, specified without choosing an enumeration.

Equations

• LongGapsBetweenPrimes.ConsecutivePrimes p q = (Nat.Prime p ∧ Nat.Prime q ∧ p < q ∧ ∀ (r : ℕ), p < r → r < q → ¬Nat.Prime r)

def LongGapsBetweenPrimes.LongGapTheorem : Prop

The precise conclusion to be proved.

Equations

• One or more equations did not get rendered due to their size.

def LongGapsBetweenPrimes.ShortTranslates : Prop

The short-translate assertion of Proposition 1.2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongGapsBetweenPrimes.normalizer (P : ℕ) : ℝ

The normalization B in (3.1).

Equations

• LongGapsBetweenPrimes.normalizer P = ∑ d ∈ P.divisors.erase 1, 1 / (↑d.totient * Real.log ↑d)

noncomputable def LongGapsBetweenPrimes.coefficient (P d : ℕ) : ℝ

The coefficient a(d) in (3.1).

Equations

• LongGapsBetweenPrimes.coefficient P d = if d = 1 then 1 else -1 / (LongGapsBetweenPrimes.normalizer P * Real.log ↑d)

theorem LongGapsBetweenPrimes.one_lt_of_mem_divisors_erase_one {P d : ℕ} (hd : d ∈ P.divisors.erase 1) : 1 < d

A divisor other than one is greater than one.

theorem LongGapsBetweenPrimes.normalizer_pos {P : ℕ} (hP : 1 < P) : 0 < normalizer P

The normalizer is positive when P > 1.

theorem LongGapsBetweenPrimes.coefficient_neg {P d : ℕ} (hP : 1 < P) (hd : 1 < d) : coefficient P d < 0

For P > 1, coefficients at d > 1 are negative.

theorem LongGapsBetweenPrimes.coefficient_cancellation {P : ℕ} (hP : 1 < P) : ∑ d ∈ P.divisors, coefficient P d / ↑d.totient = 0

Exact cancellation, equations (3.2) and (3.5).

theorem LongGapsBetweenPrimes.partial_cancellation {P : ℕ} (hP : 1 < P) (E : Finset ℕ) (hE : E ⊆ P.divisors) (h1 : 1 ∈ E) : ∑ d ∈ E, coefficient P d / ↑d.totient = ∑ d ∈ P.divisors \ E, |coefficient P d| / ↑d.totient

The omitted terms in (3.11) have positive total mass.

theorem LongGapsBetweenPrimes.partial_cancellation_nonneg {P : ℕ} (hP : 1 < P) (E : Finset ℕ) (hE : E ⊆ P.divisors) (h1 : 1 ∈ E) : 0 ≤ ∑ d ∈ E, coefficient P d / ↑d.totient

A divisor subsum containing one has nonnegative weighted coefficient sum.

noncomputable def LongGapsBetweenPrimes.residueFactor {p : ℕ} (a t : Fin p) : ℝ

The local factor as a function of a residue class with specified root.

Equations

• LongGapsBetweenPrimes.residueFactor a t = if t = a then -1 else 1 / (↑p - 1)

theorem LongGapsBetweenPrimes.sum_one_exception {p : ℕ} (a : Fin p) (c d : ℝ) : (∑ t : Fin p, if t = a then c else d) = c + (↑p - 1) * d

Sum a constant function with one exceptional value.

theorem LongGapsBetweenPrimes.sum_residueFactor {p : ℕ} (hp : 1 < p) (a : Fin p) : ∑ t : Fin p, residueFactor a t = 0

The local mean is zero (Section 3.1).

theorem LongGapsBetweenPrimes.sum_residueFactor_sq {p : ℕ} (hp : 1 < p) (a : Fin p) : ∑ t : Fin p, residueFactor a t ^ 2 = ↑p / (↑p - 1)

The local square mean is 1/(p-1), before dividing the sum by p.

theorem LongGapsBetweenPrimes.sum_residueFactor_mul {p : ℕ} (hp : 1 < p) (a b : Fin p) (hab : a ≠ b) : ∑ t : Fin p, residueFactor a t * residueFactor b t = -↑p / (↑p - 1) ^ 2

Distinct roots have negative covariance, as used in (3.9).

theorem LongGapsBetweenPrimes.totient_eq_prod_sub_one_of_squarefree {d : ℕ} (hd : Squarefree d) : d.totient = ∏ p ∈ d.primeFactors, (p - 1)

For squarefree d, its totient is the product of p - 1 over its prime factors.

noncomputable def LongGapsBetweenPrimes.coefficientMoment (P : ℕ) (γ : ℝ) : ℝ

A_gamma in Lemma 3.1; A is its value at gamma = 0.

Equations

• LongGapsBetweenPrimes.coefficientMoment P γ = ∑ d ∈ P.divisors, LongGapsBetweenPrimes.coefficient P d ^ 2 * ↑d ^ γ / ↑d.totient

noncomputable def LongGapsBetweenPrimes.coefficientAbsMoment (P : ℕ) (γ : ℝ) : ℝ

The absolute coefficient moment over nontrivial divisors.

Equations

• LongGapsBetweenPrimes.coefficientAbsMoment P γ = ∑ d ∈ P.divisors.erase 1, |LongGapsBetweenPrimes.coefficient P d| * ↑d ^ γ / ↑d.totient

theorem LongGapsBetweenPrimes.coefficientMoment_zero (P : ℕ) : coefficientMoment P 0 = ∑ d ∈ P.divisors, coefficient P d ^ 2 / ↑d.totient

Expand the coefficient moment at exponent zero.

theorem LongGapsBetweenPrimes.coefficientMoment_ge_one {P : ℕ} (hP : P ≠ 0) (γ : ℝ) : 1 ≤ coefficientMoment P γ

The divisor one gives a lower bound of one for the coefficient moment.

theorem LongGapsBetweenPrimes.exp_sub_one_le_mul_exp (x : ℝ) : Real.exp x - 1 ≤ x * Real.exp x

The exponential increment is at most x * exp x.

theorem LongGapsBetweenPrimes.rpow_sub_one_le {v γ : ℝ} (hv : 0 < v) : v ^ γ - 1 ≤ γ * v ^ γ * Real.log v

The power increment is at most γ * v ^ γ * log v.

theorem LongGapsBetweenPrimes.coefficient_sq_mul_log {P d : ℕ} (hP : 1 < P) (hd : 1 < d) : coefficient P d ^ 2 * Real.log ↑d = |coefficient P d| / normalizer P

A squared coefficient times log d equals its normalized absolute value.

theorem LongGapsBetweenPrimes.coefficientMoment_sub_le {P : ℕ} (hP : 1 < P) (γ : ℝ) : coefficientMoment P γ - coefficientMoment P 0 ≤ γ / normalizer P * coefficientAbsMoment P γ

Control the change in the squared moment by the absolute moment.

theorem LongGapsBetweenPrimes.moment_tail_le {α : Type u_1} (s : Finset α) (f v : α → ℝ) (D β : ℝ) (hD : 0 < D) (hβ : 0 ≤ β) (hf : ∀ a ∈ s, 0 ≤ f a) (hv : ∀ a ∈ s, 0 ≤ v a) : ∑ a ∈ s with D < v a, f a ≤ D ^ (-β) * ∑ a ∈ s, f a * v a ^ β

Rankin's tail estimate, in the finite form needed for (3.10).

@[reducible, inline]

abbrev LongGapsBetweenPrimes.DivisorIndex (P : ℕ) : Type

Divisors regarded as a finite index type.

Equations

• LongGapsBetweenPrimes.DivisorIndex P = ↥P.divisors

@[reducible, inline]

abbrev LongGapsBetweenPrimes.DivisorTuple (P k : ℕ) : Type

Tuples of k divisors of P.

Equations

• LongGapsBetweenPrimes.DivisorTuple P k = (Fin k → LongGapsBetweenPrimes.DivisorIndex P)

def LongGapsBetweenPrimes.tupleProduct {P k : ℕ} (r : DivisorTuple P k) : ℕ

The product of the divisors in a tuple.

Equations

• LongGapsBetweenPrimes.tupleProduct r = ∏ i : Fin k, ↑(r i)

noncomputable def LongGapsBetweenPrimes.tupleRegion (P k : ℕ) (D : ℝ) : Finset (DivisorTuple P k)

The common truncated region R_k of (3.3).

Equations

• LongGapsBetweenPrimes.tupleRegion P k D = {r : LongGapsBetweenPrimes.DivisorTuple P k | (∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) ∧ ↑(LongGapsBetweenPrimes.tupleProduct r) ≤ D}

noncomputable def LongGapsBetweenPrimes.tupleMass {P k : ℕ} (r : DivisorTuple P k) : ℝ

The diagonal mass attached to one tuple in (3.9).

Equations

• LongGapsBetweenPrimes.tupleMass r = ∏ i : Fin k, LongGapsBetweenPrimes.coefficient P ↑(r i) ^ 2 / ↑(↑(r i)).totient

theorem LongGapsBetweenPrimes.tupleMass_nonneg {P k : ℕ} (r : DivisorTuple P k) : 0 ≤ tupleMass r

The diagonal mass of a divisor tuple is nonnegative.

theorem LongGapsBetweenPrimes.sum_divisorIndex (P : ℕ) (f : ℕ → ℝ) : ∑ d : DivisorIndex P, f ↑d = ∑ d ∈ P.divisors, f d

Rewrite a sum over divisor indices as a sum over the divisor finset.

theorem LongGapsBetweenPrimes.sum_tupleMass (P k : ℕ) : ∑ r : DivisorTuple P k, tupleMass r = coefficientMoment P 0 ^ k

The total tuple mass is the kth power of the zero coefficient moment.

theorem LongGapsBetweenPrimes.sum_tupleMass_mul_rpow (P k : ℕ) (γ : ℝ) : ∑ r : DivisorTuple P k, tupleMass r * ↑(tupleProduct r) ^ γ = coefficientMoment P γ ^ k

The tilted tuple mass factors as a power of the coefficient moment.

theorem LongGapsBetweenPrimes.diagonal_tail_le (P k : ℕ) {D β : ℝ} (hD : 0 < D) (hβ : 0 ≤ β) : ∑ r : DivisorTuple P k with D < ↑(tupleProduct r), tupleMass r ≤ D ^ (-β) * coefficientMoment P β ^ k

The first inequality in (3.10), with no asymptotic assumptions.

theorem LongGapsBetweenPrimes.pow_le_mul_exp {A B t : ℝ} (hA : 1 ≤ A) (hB : 0 ≤ B) (ht : 0 ≤ t) (hBA : B ≤ A + t) (k : ℕ) : B ^ k ≤ A ^ k * Real.exp (↑k * t)

Convert an additive bound into an exponential bound on powers.

theorem LongGapsBetweenPrimes.coefficientMoment_pow_le {P : ℕ} (hP : 1 < P) {C γ : ℝ} (hC : 0 ≤ C) (hγ : 0 ≤ γ) (hM : coefficientAbsMoment P γ ≤ C * normalizer P) (k : ℕ) : coefficientMoment P γ ^ k ≤ coefficientMoment P 0 ^ k * Real.exp (↑k * C * γ)

Bound powers of a tilted coefficient moment relative to the zero moment.

theorem LongGapsBetweenPrimes.consecutivePrimes_of_composite_interval {N H : ℕ} (hN : 2 ≤ N) (hcomposite : ∀ (n : ℕ), N < n → n ≤ N + H → ¬Nat.Prime n) : ∃ (p : ℕ) (q : ℕ), ConsecutivePrimes p q ∧ p ≤ N ∧ N + H < q ∧ q ≤ 2 * N ∧ H < q - p

The elementary passage from a prime-free interval to consecutive primes. Bertrand's postulate supplies the upper endpoint bound used in Section 2.

theorem LongGapsBetweenPrimes.prime_or_smooth_of_survives {n H : ℕ} {x w z : ℝ} (hn : 1 ≤ n) (hnH : n ≤ H) (hx : 0 < x) (hsmall : 2 * ↑H < x * w) (hsurvives : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ w ∨ z < ↑p ∧ ↑p ≤ x / 2 → ¬p ∣ n) : Nat.Prime n ∨ ∀ (p : ℕ), Nat.Prime p → p ∣ n → ↑p ≤ z

The initial zero-residue sieve leaves only primes and z-smooth integers.

def LongGapsBetweenPrimes.survivors (S ps : Finset ℕ) (a : ℕ → ℕ) : Finset ℕ

Elements of S avoiding the selected residue classes.

Equations

• LongGapsBetweenPrimes.survivors S ps a = {n ∈ S | ∀ p ∈ ps, n % p ≠ a p}

theorem LongGapsBetweenPrimes.greedy_residue_classes (S ps : Finset ℕ) (hpos : ∀ p ∈ ps, 0 < p) : ∃ (a : ℕ → ℕ), (∀ p ∈ ps, a p < p) ∧ ↑(survivors S ps a).card ≤ ↑S.card * ∏ p ∈ ps, (1 - 1 / ↑p)

The greedy product bound in (2.1), before applying Mertens' estimate.

theorem LongGapsBetweenPrimes.abs_quadratic_form_le_rows {ι : Type u_1} [Fintype ι] (c : ι → ℝ) (K : ι → ι → ℝ) (hK : ∀ (i j : ι), |K i j| = |K j i|) : |∑ i : ι, ∑ j : ι, c i * c j * K i j| ≤ ∑ i : ι, c i ^ 2 * ∑ j : ι, |K i j|

A symmetric matrix is controlled by its absolute row sums. This is the 2|ab| ≤ a²+b² argument invoked in the proof of (3.9).

theorem LongGapsBetweenPrimes.quadratic_form_near_diagonal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ι → ℝ) (K : ι → ι → ℝ) (ε : ℝ) (hsym : ∀ (i j : ι), K i j = K j i) (hdiag : ∀ (i : ι), K i i = 1) (hrow : ∀ (i : ι), (∑ j : ι, if j = i then 0 else |K i j|) ≤ ε) : |∑ i : ι, ∑ j : ι, c i * c j * K i j - ∑ i : ι, c i ^ 2| ≤ ε * ∑ i : ι, c i ^ 2

Row sums away from the diagonal bound the quadratic error from the identity.

def LongGapsBetweenPrimes.productBasis {α : Type u_1} [Fintype α] {Ω : α → Type u_2} {J : α → Type u_3} (f : (p : α) → J p → Ω p → ℝ) (σ : (p : α) → J p) (t : (p : α) → Ω p) : ℝ

The product of selected local basis functions over all coordinates.

Equations

• LongGapsBetweenPrimes.productBasis f σ t = ∏ p : α, f p (σ p) (t p)

theorem LongGapsBetweenPrimes.average_residueFactor {p : ℕ} (hp : 1 < p) (a : Fin p) : Finset.univ.expect (residueFactor a) = 0

The residue factor has mean zero.

theorem LongGapsBetweenPrimes.average_residueFactor_sq {p : ℕ} (hp : 1 < p) (a : Fin p) : (Finset.univ.expect fun (t : Fin p) => residueFactor a t ^ 2) = 1 / (↑p - 1)

The residue factor has second moment 1 / (p - 1).

theorem LongGapsBetweenPrimes.average_residueFactor_mul {p : ℕ} (hp : 1 < p) (a b : Fin p) (hab : a ≠ b) : (Finset.univ.expect fun (t : Fin p) => residueFactor a t * residueFactor b t) = -1 / (↑p - 1) ^ 2

Distinct residue factors have covariance -1 / (p - 1)^2.

noncomputable def LongGapsBetweenPrimes.localBasis {p k : ℕ} (root : Fin k → Fin p) (i : Option (Fin k)) (t : Fin p) : ℝ

The constant function and residue factors scaled to have variance one.

Equations

• LongGapsBetweenPrimes.localBasis root none t = 1
• LongGapsBetweenPrimes.localBasis root (some j) t = √(↑p - 1) * LongGapsBetweenPrimes.residueFactor (root j) t

noncomputable def LongGapsBetweenPrimes.localKernel (p : ℕ) {k : ℕ} (i j : Option (Fin k)) : ℝ

The Gram kernel for the normalized local basis.

Equations

• LongGapsBetweenPrimes.localKernel p none none = 1
• LongGapsBetweenPrimes.localKernel p none (some val) = 0
• LongGapsBetweenPrimes.localKernel p (some val) none = 0
• LongGapsBetweenPrimes.localKernel p (some a) (some b) = if a = b then 1 else -1 / (↑p - 1)

theorem LongGapsBetweenPrimes.average_localBasis_mul {p k : ℕ} (hp : 1 < p) (root : Fin k → Fin p) (hroot : Function.Injective root) (i j : Option (Fin k)) : (Finset.univ.expect fun (t : Fin p) => localBasis root i t * localBasis root j t) = localKernel p i j

The local Gram matrix, with the nonconstant factors normalized to variance one.

noncomputable def LongGapsBetweenPrimes.localRow (p k : ℕ) (i : Option (Fin k)) : ℝ

The absolute row sum of the local Gram kernel.

Equations

• LongGapsBetweenPrimes.localRow p k none = 1
• LongGapsBetweenPrimes.localRow p k (some j) = 1 + (↑k - 1) / (↑p - 1)

theorem LongGapsBetweenPrimes.localKernel_symm (p : ℕ) {k : ℕ} (i j : Option (Fin k)) : localKernel p i j = localKernel p j i

The local Gram kernel is symmetric.

theorem LongGapsBetweenPrimes.localKernel_diag (p : ℕ) {k : ℕ} (i : Option (Fin k)) : localKernel p i i = 1

The local Gram kernel has diagonal entries equal to one.

theorem LongGapsBetweenPrimes.sum_abs_localKernel {p k : ℕ} (hp : 1 < p) (i : Option (Fin k)) : ∑ j : Option (Fin k), |localKernel p i j| = localRow p k i

Summing the absolute local kernel entries gives localRow.

noncomputable def LongGapsBetweenPrimes.productKernel {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ τ : α → Option (Fin k)) : ℝ

The product of local Gram kernels over all coordinates.

Equations

• LongGapsBetweenPrimes.productKernel size σ τ = ∏ p : α, LongGapsBetweenPrimes.localKernel (size p) (σ p) (τ p)

theorem LongGapsBetweenPrimes.productKernel_symm {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ τ : α → Option (Fin k)) : productKernel size σ τ = productKernel size τ σ

The product Gram kernel is symmetric.

theorem LongGapsBetweenPrimes.productKernel_diag {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ : α → Option (Fin k)) : productKernel size σ σ = 1

The product Gram kernel has diagonal entries equal to one.

theorem LongGapsBetweenPrimes.sum_abs_productKernel {α : Type u_1} [Fintype α] [DecidableEq α] (size : α → ℕ) (hsize : ∀ (p : α), 1 < size p) {k : ℕ} (σ : α → Option (Fin k)) : ∑ τ : α → Option (Fin k), |productKernel size σ τ| = ∏ p : α, localRow (size p) k (σ p)

The product of local row sums from the proof of (3.9).

theorem LongGapsBetweenPrimes.average_productBasis_localBasis {α : Type u_1} [Fintype α] [DecidableEq α] (size : α → ℕ) (hsize : ∀ (p : α), 1 < size p) {k : ℕ} (root : (p : α) → Fin k → Fin (size p)) (hroot : ∀ (p : α), Function.Injective (root p)) (σ τ : α → Option (Fin k)) : (Finset.univ.expect fun (t : (p : α) → Fin (size p)) => productBasis (fun (p : α) => localBasis (root p)) σ t * productBasis (fun (p : α) => localBasis (root p)) τ t) = productKernel size σ τ

Products of local basis functions have Gram kernel productKernel.

def LongGapsBetweenPrimes.assignmentSupport {α : Type u_1} [Fintype α] {k : ℕ} (σ : α → Option (Fin k)) : Finset α

Coordinates assigned to a nonconstant local basis function.

Equations

• LongGapsBetweenPrimes.assignmentSupport σ = {p : α | (σ p).isSome = true}

def LongGapsBetweenPrimes.assignmentProduct {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ : α → Option (Fin k)) : ℕ

The product of coordinate sizes on an assignment's support.

Equations

• LongGapsBetweenPrimes.assignmentProduct size σ = ∏ p ∈ LongGapsBetweenPrimes.assignmentSupport σ, size p

theorem LongGapsBetweenPrimes.assignment_row_bound {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (hk : 1 ≤ k) (σ : α → Option (Fin k)) {z D : ℝ} (hz : 1 < z) (hsize : ∀ (p : α), z ≤ ↑(size p)) (hcut : ↑(assignmentProduct size σ) ≤ D) : ∏ p : α, localRow (size p) k (σ p) ≤ Real.exp (↑k * Real.log D / ((z - 1) * Real.log z))

The cutoff controls the row sums uniformly, independently of the number of auxiliary primes in P.

def LongGapsBetweenPrimes.residueIndicator (m a n : ℕ) : ℝ

The indicator of the residue class a modulo m.

Equations

• LongGapsBetweenPrimes.residueIndicator m a n = if n % m = a then 1 else 0

theorem LongGapsBetweenPrimes.residue_count_error_le_one {m a : ℕ} (ha : a < m) (T : ℕ) : |∑ n ∈ Finset.range T, residueIndicator m a n - ↑T / ↑m| ≤ 1

The error of counting one congruence class is at most one.

theorem LongGapsBetweenPrimes.residue_average_error {m a T : ℕ} (ha : a < m) (hT : 0 < T) : |(∑ n ∈ Finset.range T, residueIndicator m a n) / ↑T - 1 / ↑m| ≤ 1 / ↑T

A residue class has frequency error at most 1 / T on an interval of length T.

theorem LongGapsBetweenPrimes.weighted_union_bound {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] (w : Ω → ℝ) (event : ι → Ω → Prop) [(i : ι) → DecidablePred (event i)] (hw : ∀ (t : Ω), 0 ≤ w t) : (∑ t : Ω, w t * if ∃ (i : ι), event i t then 1 else 0) ≤ ∑ i : ι, ∑ t : Ω, w t * if event i t then 1 else 0

A weighted union bound, stated without a probability-space interface.

theorem LongGapsBetweenPrimes.sum_pair_marked_product {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (w : Ω → ℝ) (hw : ∑ d : Ω, w d = 1) (mark : Ω → Prop) [DecidablePred mark] (i j : ι) (hij : i ≠ j) : (∑ r : ι → Ω, (∏ ℓ : ι, w (r ℓ)) * if mark (r i) ∧ mark (r j) then 1 else 0) = (∑ d : Ω, w d * if mark d then 1 else 0) ^ 2

Independence of two marked coordinates under a product of normalized masses.

theorem LongGapsBetweenPrimes.product_collision_bound {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] (w : Ω → ℝ) (hw : ∀ (d : Ω), 0 ≤ w d) (hsum : ∑ d : Ω, w d = 1) (mark : α → Ω → Prop) [(p : α) → DecidablePred (mark p)] (k : ℕ) : (∑ r : Fin k → Ω, (∏ i : Fin k, w (r i)) * if ∃ (p : α) (i : Fin k) (j : Fin k), i ≠ j ∧ mark p (r i) ∧ mark p (r j) then 1 else 0) ≤ ↑k ^ 2 * ∑ p : α, (∑ d : Ω, w d * if mark p d then 1 else 0) ^ 2

The collision estimate for independently chosen divisors: a common mark in two coordinates costs at most the square of its one-coordinate mass.

theorem LongGapsBetweenPrimes.sum_divisors_dvd_eq {P p : ℕ} (hP : P ≠ 0) (hp : 0 < p) (hpP : p ∣ P) (f : ℕ → ℝ) : ∑ d ∈ P.divisors with p ∣ d, f d = ∑ e ∈ (P / p).divisors, f (p * e)

Divisors divisible by p are parametrized by the divisors of P/p.

theorem LongGapsBetweenPrimes.abs_coefficient_mul_le {P p e : ℕ} (hP : 1 < P) (hp : 1 ≤ p) (he : 1 < e) : |coefficient P (p * e)| ≤ |coefficient P e|

Multiplying a nontrivial divisor by a prime decreases the absolute coefficient.

theorem LongGapsBetweenPrimes.coefficientAbsMoment_zero {P : ℕ} (hP : 1 < P) : coefficientAbsMoment P 0 = 1

The absolute coefficient moment at exponent zero equals one.

theorem LongGapsBetweenPrimes.sum_abs_coefficient_div_totient {P : ℕ} (hP : 1 < P) : ∑ d ∈ P.divisors, |coefficient P d| / ↑d.totient = 2

The sum of absolute coefficients divided by totients equals two.

theorem LongGapsBetweenPrimes.coefficient_prime_incidence {P p : ℕ} (hP : 1 < P) (hsq : Squarefree P) (hp : Nat.Prime p) (hpP : p ∣ P) (hcoeff : |coefficient P p| ≤ 1) : ∑ d ∈ P.divisors with p ∣ d, |coefficient P d| / ↑d.totient ≤ 4 / ↑p

The incidence bound (3.7), with an explicit constant once |a(p)| ≤ 1.

theorem LongGapsBetweenPrimes.sum_log_prime_divisors_le_log {n N : ℕ} (hn : 0 < n) (hnN : n ≤ N) : (∑ p ∈ N.primesLE, if p ∣ n then Real.log ↑p else 0) ≤ Real.log ↑n

The logarithms of distinct prime divisors sum to at most log n.

theorem LongGapsBetweenPrimes.sum_prime_log_div_le {N : ℕ} (hN : 1 ≤ N) : ∑ p ∈ N.primesLE, Real.log ↑p / ↑p ≤ Real.log ↑N + Real.log 4

An elementary upper bound for the logarithmically weighted prime harmonic sum.

noncomputable def LongGapsBetweenPrimes.eulerProduct (N : ℕ) (σ : ℝ) : ℝ

The finite Euler product over primes at most N.

Equations

• LongGapsBetweenPrimes.eulerProduct N σ = ∏ p ∈ N.primesLE, (1 - ↑p ^ (-σ))⁻¹

noncomputable def LongGapsBetweenPrimes.natPowerHom (σ : ℝ) : ℕ →* ℝ

The multiplicative weight n ↦ n ^ (-σ).

Equations

• LongGapsBetweenPrimes.natPowerHom σ = { toFun := fun (n : ℕ) => ↑n ^ (-σ), map_one' := ⋯, map_mul' := ⋯ }

theorem LongGapsBetweenPrimes.sum_smooth_le_eulerProduct {N : ℕ} {σ : ℝ} (hσ : 0 < σ) (S : Finset ℕ) (hS : ∀ n ∈ S, n ∈ (N + 1).smoothNumbers) : ∑ n ∈ S, ↑n ^ (-σ) ≤ eulerProduct N σ

The weighted sum over smooth numbers is bounded by the finite Euler product.

theorem LongGapsBetweenPrimes.log_le_eulerProduct_one (N : ℕ) : Real.log ↑N ≤ eulerProduct N 1

The lower half of the weak Mertens product estimate.

theorem LongGapsBetweenPrimes.tsum_succ_rpow_le {σ : ℝ} (hσ : 1 < σ) : ∑' (n : ℕ), (↑n + 1) ^ (-σ) ≤ 1 + 1 / (σ - 1)

The elementary zeta-function bound obtained by integrating t^(-σ).

theorem LongGapsBetweenPrimes.eulerProduct_le_zeta_bound {σ : ℝ} (hσ : 1 < σ) (N : ℕ) : eulerProduct N σ ≤ 1 + 1 / (σ - 1)

For σ > 1, the finite Euler product is at most 1 + 1 / (σ - 1).

theorem LongGapsBetweenPrimes.euler_factor_comparison {p r : ℝ} (hp : 2 ≤ p) (hr : 0 ≤ r) : (1 - p ^ (-1))⁻¹ ≤ (1 - p ^ (-(1 + r)))⁻¹ * Real.exp (2 * r * Real.log p / p)

Compare an Euler factor at exponent one with its shift by r.

theorem LongGapsBetweenPrimes.eulerProduct_comparison (N : ℕ) {r : ℝ} (hr : 0 ≤ r) : eulerProduct N 1 ≤ eulerProduct N (1 + r) * Real.exp (2 * r * ∑ p ∈ N.primesLE, Real.log ↑p / ↑p)

Moving the Euler product to the right of its pole has bounded cost.

theorem LongGapsBetweenPrimes.eulerProduct_one_le {N : ℕ} (hN : 2 ≤ N) : eulerProduct N 1 ≤ Real.exp 6 * (1 + Real.log ↑N)

An explicit weak Mertens upper bound, sufficient throughout the proof.

noncomputable def LongGapsBetweenPrimes.divisorEulerMoment (P : ℕ) (γ : ℝ) : ℝ

The power moment of divisors weighted by reciprocal totients.

Equations

• LongGapsBetweenPrimes.divisorEulerMoment P γ = ∑ d ∈ P.divisors, ↑d ^ γ / ↑d.totient

theorem LongGapsBetweenPrimes.divisorEulerMoment_primeProduct (ps : Finset ℕ) (hps : ∀ p ∈ ps, Nat.Prime p) (γ : ℝ) : divisorEulerMoment (∏ p ∈ ps, p) γ = ∏ p ∈ ps, (1 + ↑p ^ γ / (↑p - 1))

Factor the divisor Euler moment of a product of distinct primes.

theorem LongGapsBetweenPrimes.eulerProduct_pos (N : ℕ) {σ : ℝ} (hσ : 0 < σ) : 0 < eulerProduct N σ

The finite Euler product is positive at every positive exponent.

theorem LongGapsBetweenPrimes.eulerProduct_antitone (N : ℕ) {σ τ : ℝ} (hσ : 0 < σ) (hστ : σ ≤ τ) : eulerProduct N τ ≤ eulerProduct N σ

The finite Euler product decreases as its positive exponent increases.

def LongGapsBetweenPrimes.auxiliaryPrimes (Z Y : ℕ) : Finset ℕ

Primes in the interval (Z, Y].

Equations

• LongGapsBetweenPrimes.auxiliaryPrimes Z Y = Y.primesLE \ Z.primesLE

def LongGapsBetweenPrimes.auxiliaryProduct (Z Y : ℕ) : ℕ

The product of primes in the interval (Z, Y].

Equations

• LongGapsBetweenPrimes.auxiliaryProduct Z Y = ∏ p ∈ LongGapsBetweenPrimes.auxiliaryPrimes Z Y, p

theorem LongGapsBetweenPrimes.auxiliaryPrimes_prime {Z Y p : ℕ} (hp : p ∈ auxiliaryPrimes Z Y) : Nat.Prime p

Every auxiliary prime is prime.

theorem LongGapsBetweenPrimes.mem_auxiliaryPrimes {Z Y p : ℕ} : p ∈ auxiliaryPrimes Z Y ↔ Nat.Prime p ∧ Z < p ∧ p ≤ Y

Membership in the auxiliary primes means primality and Z < p ≤ Y.

theorem LongGapsBetweenPrimes.auxiliaryProduct_squarefree (Z Y : ℕ) : Squarefree (auxiliaryProduct Z Y)

The auxiliary prime product is squarefree.

theorem LongGapsBetweenPrimes.auxiliaryProduct_pos (Z Y : ℕ) : 0 < auxiliaryProduct Z Y

The auxiliary prime product is positive.

theorem LongGapsBetweenPrimes.auxiliary_euler_factorization {Z Y : ℕ} (hZY : Z ≤ Y) (σ : ℝ) : (∏ p ∈ auxiliaryPrimes Z Y, (1 - ↑p ^ (-σ))⁻¹) * eulerProduct Z σ = eulerProduct Y σ

Split the Euler product at the lower cutoff Z.

theorem LongGapsBetweenPrimes.squarefree_euler_factor_ge {p t : ℝ} (hp : 1 < p) (ht : 0 < t) : (1 - p ^ (-(1 + t)))⁻¹ ≤ 1 + p ^ (-t) / (p - 1)

A squarefree Euler factor dominates the corresponding shifted geometric factor.

theorem LongGapsBetweenPrimes.divisorEulerMoment_ge_eulerProduct {Z Y : ℕ} (hZY : Z ≤ Y) {t : ℝ} (ht : 0 < t) : eulerProduct Y (1 + t) ≤ divisorEulerMoment (auxiliaryProduct Z Y) (-t) * eulerProduct Z (1 + t)

A lower bound for the squarefree-divisor Euler product by a usual Euler product.

theorem LongGapsBetweenPrimes.eulerProduct_ge_power_integral (Y : ℕ) {t : ℝ} (ht : 0 < t) : (1 - (↑Y + 1) ^ (-t)) / t ≤ eulerProduct Y (1 + t)

Bound the Euler product below by an integral of a negative power.

theorem LongGapsBetweenPrimes.eulerProduct_ge_one_div_two_mul (Y : ℕ) {t : ℝ} (ht : 0 < t) (hscale : 1 ≤ t * Real.log (↑Y + 1)) : 1 / (2 * t) ≤ eulerProduct Y (1 + t)

The Euler product at 1 + t is at least 1 / (2 * t) when t * log (Y + 1) ≥ 1.

theorem LongGapsBetweenPrimes.divisorEulerMoment_nonneg (P : ℕ) (γ : ℝ) : 0 ≤ divisorEulerMoment P γ

The divisor Euler moment is nonnegative.

theorem LongGapsBetweenPrimes.divisorEulerMoment_lower {Z Y : ℕ} (hZY : Z ≤ Y) {t A : ℝ} (ht : 0 < t) (hA : 0 < A) (hZA : eulerProduct Z 1 ≤ A) (hscale : 1 ≤ t * Real.log (↑Y + 1)) : 1 / (2 * t * A) ≤ divisorEulerMoment (auxiliaryProduct Z Y) (-t)

The lower bound whose integral supplies a positive normalization B.

theorem LongGapsBetweenPrimes.continuous_divisorEulerMoment (P : ℕ) : Continuous fun (t : ℝ) => divisorEulerMoment P (-t)

The negatively tilted divisor Euler moment is continuous.

theorem LongGapsBetweenPrimes.integral_exp_decay_le {L a : ℝ} (hL : 0 < L) (ha : 0 ≤ a) (b : ℝ) : ∫ (t : ℝ) in a..b, Real.exp (-L * t) ≤ 1 / L

An exponential decay integral starting at a nonnegative point is at most 1 / L.

theorem LongGapsBetweenPrimes.normalizer_integral_le {P : ℕ} (hP : P ≠ 0) {a : ℝ} (ha : 0 ≤ a) (b : ℝ) : ∫ (t : ℝ) in a..b, divisorEulerMoment P (-t) - 1 ≤ normalizer P

The normalizer dominates every positive-half-line integral of U_(-t)-1.

theorem LongGapsBetweenPrimes.normalizer_lower_integral {Z Y : ℕ} (hZY : Z ≤ Y) {A a b : ℝ} (hA : 0 < A) (ha : 0 < a) (hab : a ≤ b) (hZA : eulerProduct Z 1 ≤ A) (hscale : 1 ≤ a * Real.log (↑Y + 1)) : (Real.log b - Real.log a) / (2 * A) - (b - a) ≤ normalizer (auxiliaryProduct Z Y)

Integrating the lower Euler-product bound gives a completely finite lower bound for B; no sieve asymptotic is assumed.

theorem LongGapsBetweenPrimes.normalizer_lower_bound {Z Y : ℕ} (hZY : Z ≤ Y) {A : ℝ} (hA : 0 < A) (hZA : eulerProduct Z 1 ≤ A) (hAY : A ≤ Real.log (↑Y + 1)) : Real.log (Real.log (↑Y + 1)) - Real.log A - 2 ≤ 2 * A * normalizer (auxiliaryProduct Z Y)

A logarithmic lower bound for the auxiliary normalizer.

theorem LongGapsBetweenPrimes.abs_coefficient_eq {P d : ℕ} (hP : 1 < P) (hd : 1 < d) : |coefficient P d| = 1 / (normalizer P * Real.log ↑d)

A nontrivial coefficient has absolute value 1 / (normalizer P * log d).

theorem LongGapsBetweenPrimes.coefficientAbsMoment_le {P Y : ℕ} (hP : 1 < P) (hY : 1 < Y) {γ E : ℝ} (hγ : 0 ≤ γ) (hYE : ↑Y ^ γ ≤ E) : coefficientAbsMoment P γ ≤ E + divisorEulerMoment P γ / (normalizer P * Real.log ↑Y)

Splitting at Y gives the tilted absolute-moment bound in (3.6).

theorem LongGapsBetweenPrimes.divisorEulerMoment_zero_factorization {Z Y : ℕ} (hZY : Z ≤ Y) : divisorEulerMoment (auxiliaryProduct Z Y) 0 * eulerProduct Z 1 = eulerProduct Y 1

At exponent zero, the auxiliary divisor moment is an Euler-product ratio.

theorem LongGapsBetweenPrimes.divisorEulerMoment_zero_le {Z Y : ℕ} (hZY : Z ≤ Y) (hZ : 2 ≤ Z) : divisorEulerMoment (auxiliaryProduct Z Y) 0 ≤ Real.exp 6 * (1 + Real.log ↑Y) / Real.log ↑Z

Bound the auxiliary zero moment by a ratio of logarithms.

theorem LongGapsBetweenPrimes.squarefree_euler_factor_tilt {p γ E : ℝ} (hp : 1 < p) (hγ : 0 ≤ γ) (hpE : p ^ γ ≤ E) : 1 + p ^ γ / (p - 1) ≤ (1 + 1 / (p - 1)) * Real.exp (E * γ * Real.log p / p)

An exponential bound for tilting a squarefree Euler factor.

theorem LongGapsBetweenPrimes.divisorEulerMoment_tilt (ps : Finset ℕ) (hps : ∀ p ∈ ps, Nat.Prime p) {γ E : ℝ} (hγ : 0 ≤ γ) (hE : ∀ p ∈ ps, ↑p ^ γ ≤ E) : divisorEulerMoment (∏ p ∈ ps, p) γ ≤ divisorEulerMoment (∏ p ∈ ps, p) 0 * Real.exp (E * γ * ∑ p ∈ ps, Real.log ↑p / ↑p)

Tilting a squarefree divisor moment costs an exponential factor.

theorem LongGapsBetweenPrimes.auxiliary_divisorEulerMoment_tilt {Z Y : ℕ} (hY : 2 ≤ Y) {γ : ℝ} (hγ : 0 ≤ γ) (hscale : γ * Real.log ↑Y ≤ 2) : divisorEulerMoment (auxiliaryProduct Z Y) γ ≤ divisorEulerMoment (auxiliaryProduct Z Y) 0 * Real.exp (6 * Real.exp 2)

Uniformly bound the cost of tilting the auxiliary divisor moment.

theorem LongGapsBetweenPrimes.prime_dvd_auxiliaryProduct {Z Y p : ℕ} (hp : Nat.Prime p) (hdvd : p ∣ auxiliaryProduct Z Y) : p ∈ auxiliaryPrimes Z Y

Every prime divisor of the auxiliary product is an auxiliary prime.

theorem LongGapsBetweenPrimes.auxiliary_divisor_gt {Z Y d : ℕ} (hd : d ∈ (auxiliaryProduct Z Y).divisors.erase 1) : Z < d

Every nontrivial auxiliary divisor exceeds the lower cutoff Z.

theorem LongGapsBetweenPrimes.auxiliary_coefficient_le_one {Z Y : ℕ} (hP : 1 < auxiliaryProduct Z Y) (hZ : 1 < Z) (hB : 1 ≤ normalizer (auxiliaryProduct Z Y) * Real.log ↑Z) {d : ℕ} (hd : d ∈ (auxiliaryProduct Z Y).divisors) : |coefficient (auxiliaryProduct Z Y) d| ≤ 1

A normalizer lower bound makes every auxiliary coefficient at most one in magnitude.

noncomputable def LongGapsBetweenPrimes.absoluteMomentBound (b : ℝ) : ℝ

An explicit absolute moment bound from a lower bound on the normalizer.

Equations

• LongGapsBetweenPrimes.absoluteMomentBound b = Real.exp 2 + 2 * Real.exp 6 * Real.exp (6 * Real.exp 2) / b

noncomputable def LongGapsBetweenPrimes.coefficientControl (b : ℝ) : ℝ

The absolute moment bound divided by the normalizer lower bound.

Equations

• LongGapsBetweenPrimes.coefficientControl b = LongGapsBetweenPrimes.absoluteMomentBound b / b

theorem LongGapsBetweenPrimes.absoluteMomentBound_pos {b : ℝ} (hb : 0 < b) : 0 < absoluteMomentBound b

The absolute moment bound is positive for positive b.

theorem LongGapsBetweenPrimes.coefficientControl_pos {b : ℝ} (hb : 0 < b) : 0 < coefficientControl b

The coefficient control constant is positive for positive b.

theorem LongGapsBetweenPrimes.auxiliary_coefficientAbsMoment_le {Z Y : ℕ} (hZY : Z ≤ Y) (hZ : 2 ≤ Z) (hlogZ : 1 ≤ Real.log ↑Z) (hP : 1 < auxiliaryProduct Z Y) {b γ : ℝ} (hb : 0 < b) (hB : b ≤ normalizer (auxiliaryProduct Z Y)) (hγ : 0 ≤ γ) (hscale : γ * Real.log ↑Y ≤ 2) : coefficientAbsMoment (auxiliaryProduct Z Y) γ ≤ absoluteMomentBound b

Bound the auxiliary absolute moment by absoluteMomentBound.

theorem LongGapsBetweenPrimes.auxiliary_coefficientAbsMoment_control {Z Y : ℕ} (hZY : Z ≤ Y) (hZ : 2 ≤ Z) (hlogZ : 1 ≤ Real.log ↑Z) (hP : 1 < auxiliaryProduct Z Y) {b γ : ℝ} (hb : 0 < b) (hB : b ≤ normalizer (auxiliaryProduct Z Y)) (hγ : 0 ≤ γ) (hscale : γ * Real.log ↑Y ≤ 2) : coefficientAbsMoment (auxiliaryProduct Z Y) γ ≤ coefficientControl b * normalizer (auxiliaryProduct Z Y)

Bound the auxiliary absolute moment by a constant times the normalizer.

noncomputable def LongGapsBetweenPrimes.sieveZ (x : ℝ) : ℕ

The auxiliary prime ranges of Section 3.1, with integral endpoints.

Equations

• LongGapsBetweenPrimes.sieveZ x = ⌊x ^ 6⌋₊

noncomputable def LongGapsBetweenPrimes.sieveUpperLog (x : ℝ) : ℝ

The logarithmic upper cutoff x / (log x)^5 for the sieve primes.

Equations

• LongGapsBetweenPrimes.sieveUpperLog x = x / Real.log x ^ 5

noncomputable def LongGapsBetweenPrimes.sieveY (x : ℝ) : ℕ

The upper sieve cutoff, rounded down to an integer.

Equations

• LongGapsBetweenPrimes.sieveY x = ⌊Real.exp (LongGapsBetweenPrimes.sieveUpperLog x)⌋₊

noncomputable def LongGapsBetweenPrimes.sieveP (x : ℝ) : ℕ

The product of primes between the two sieve cutoffs.

Equations

• LongGapsBetweenPrimes.sieveP x = LongGapsBetweenPrimes.auxiliaryProduct (LongGapsBetweenPrimes.sieveZ x) (LongGapsBetweenPrimes.sieveY x)

noncomputable def LongGapsBetweenPrimes.normalizerLower : ℝ

A fixed positive lower bound used for the sieve normalizer.

Equations

• LongGapsBetweenPrimes.normalizerLower = 1 / (100 * Real.exp 6)

theorem LongGapsBetweenPrimes.normalizerLower_pos : 0 < normalizerLower

The fixed normalizer lower bound is positive.

theorem LongGapsBetweenPrimes.sieve_normalizer_lower_of_bounds {x : ℝ} (hx : 0 < x) (hlx : 1 ≤ Real.log x) (hZ : 2 ≤ sieveZ x) (hlarge : 7 * Real.exp 6 * Real.log x ^ 6 ≤ x) (hsmall : 6 * Real.log (Real.log x) + Real.log 7 + 8 ≤ Real.log x / 2) : sieveZ x ≤ sieveY x ∧ normalizerLower ≤ normalizer (sieveP x)

Explicit size bounds ensure ordered cutoffs and a uniform normalizer lower bound.

theorem LongGapsBetweenPrimes.tendsto_sieveZ : Filter.Tendsto sieveZ Filter.atTop Filter.atTop

The lower sieve cutoff tends to infinity.

theorem LongGapsBetweenPrimes.tendsto_log_sieveZ : Filter.Tendsto (fun (x : ℝ) => Real.log ↑(sieveZ x)) Filter.atTop Filter.atTop

The logarithm of the lower sieve cutoff tends to infinity.

theorem LongGapsBetweenPrimes.eventually_sieve_normalizer_lower : ∀ᶠ (x : ℝ) in Filter.atTop, sieveZ x ≤ sieveY x ∧ normalizerLower ≤ normalizer (sieveP x)

The unconditional positive lower bound for B for the paper's parameters.

noncomputable def LongGapsBetweenPrimes.sieveBeta (x : ℝ) : ℝ

The tilt scale reciprocal to the logarithmic upper sieve cutoff.

Equations

• LongGapsBetweenPrimes.sieveBeta x = 1 / LongGapsBetweenPrimes.sieveUpperLog x

noncomputable def LongGapsBetweenPrimes.weightConstant : ℝ

A common constant controlling the coefficient moments.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.weightConstant_gt_one : 1 < weightConstant

The common coefficient constant exceeds one.

structure LongGapsBetweenPrimes.CoefficientEstimates (P : ℕ) (β C : ℝ) : Prop

The coefficient estimates needed by the finite weighted sieve argument.

• one_lt : 1 < P

  The sieve modulus exceeds one.

• squarefree : Squarefree P

  The sieve modulus is squarefree.

• abs_le_one (d : ℕ) : d ∈ P.divisors → |coefficient P d| ≤ 1

  Every divisor coefficient has absolute value at most one.

• absMoment_le (γ : ℝ) : 0 ≤ γ → γ ≤ 2 * β → coefficientAbsMoment P γ ≤ C

  The absolute moment is uniformly bounded for tilts up to 2 * β.

• moment_control (γ : ℝ) : 0 ≤ γ → γ ≤ 2 * β → coefficientAbsMoment P γ ≤ C * normalizer P

  The absolute moment is also controlled relative to the normalizer.

theorem LongGapsBetweenPrimes.eventually_sieve_coefficient_estimates : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < sieveBeta x ∧ CoefficientEstimates (sieveP x) (sieveBeta x) weightConstant

The sieve coefficients eventually satisfy all required uniform estimates.

noncomputable def LongGapsBetweenPrimes.divisorProbability (P : ℕ) (d : DivisorIndex P) : ℝ

Squared coefficient mass normalized to a probability on divisors.

Equations

• LongGapsBetweenPrimes.divisorProbability P d = LongGapsBetweenPrimes.coefficient P ↑d ^ 2 / ↑(↑d).totient / LongGapsBetweenPrimes.coefficientMoment P 0

theorem LongGapsBetweenPrimes.divisorProbability_nonneg {P : ℕ} (hP : P ≠ 0) (d : DivisorIndex P) : 0 ≤ divisorProbability P d

The normalized divisor mass is nonnegative.

theorem LongGapsBetweenPrimes.sum_divisorProbability {P : ℕ} (hP : P ≠ 0) : ∑ d : DivisorIndex P, divisorProbability P d = 1

The normalized divisor masses sum to one.

theorem LongGapsBetweenPrimes.tupleMass_eq_probability {P k : ℕ} (hP : P ≠ 0) (r : DivisorTuple P k) : tupleMass r = coefficientMoment P 0 ^ k * ∏ i : Fin k, divisorProbability P (r i)

Tuple mass is a fixed scale times the product of the divisor probabilities.

theorem LongGapsBetweenPrimes.divisorProbability_prime_incidence {P p : ℕ} {β C : ℝ} (h : CoefficientEstimates P β C) (hp : Nat.Prime p) (hpP : p ∣ P) : (∑ d : DivisorIndex P, divisorProbability P d * if p ∣ ↑d then 1 else 0) ≤ 4 / ↑p

A prime divides a random divisor with probability at most 4 / p.

theorem LongGapsBetweenPrimes.noncoprime_pair_iff_common_prime {P k : ℕ} (hP : P ≠ 0) (r : DivisorTuple P k) : (¬∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) ↔ ∃ (p : ↥P.primeFactors) (i : Fin k) (j : Fin k), i ≠ j ∧ ↑p ∣ ↑(r i) ∧ ↑p ∣ ↑(r j)

Failure of pairwise coprimality is witnessed by a shared prime factor.

theorem LongGapsBetweenPrimes.diagonal_collision_le {P M k : ℕ} {β C : ℝ} (h : CoefficientEstimates P β C) (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M < p) : (∑ r : DivisorTuple P k, tupleMass r * if ¬∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j) then 1 else 0) ≤ 16 * ↑k ^ 2 / ↑M * coefficientMoment P 0 ^ k

The discarded mass from tuples sharing a prime, with an explicit constant.

noncomputable def LongGapsBetweenPrimes.diagonalMass (P k : ℕ) (D : ℝ) : ℝ

The total diagonal mass over the truncated tuple region.

Equations

• LongGapsBetweenPrimes.diagonalMass P k D = ∑ r ∈ LongGapsBetweenPrimes.tupleRegion P k D, LongGapsBetweenPrimes.tupleMass r

theorem LongGapsBetweenPrimes.diagonalMass_nonneg (P k : ℕ) (D : ℝ) : 0 ≤ diagonalMass P k D

The total diagonal mass is nonnegative.

theorem LongGapsBetweenPrimes.diagonalMass_tail_collision {P M k : ℕ} {β C D : ℝ} (h : CoefficientEstimates P β C) (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M < p) (hD : 0 < D) (hβ : 0 ≤ β) : coefficientMoment P 0 ^ k - diagonalMass P k D ≤ D ^ (-β) * coefficientMoment P β ^ k + 16 * ↑k ^ 2 / ↑M * coefficientMoment P 0 ^ k

The only losses in the diagonal are the product cutoff and shared primes.

theorem LongGapsBetweenPrimes.indexed_offdiag_sum_le {ι : Type u_1} {Λ : Type u_2} [Fintype ι] [Fintype Λ] [DecidableEq ι] (σ : ι → Λ) (hσ : Function.Injective σ) (K : Λ → Λ → ℝ) (hdiag : ∀ (j : Λ), K j j = 1) (i : ι) : (∑ j : ι, if j = i then 0 else |K (σ i) (σ j)|) ≤ ∑ τ : Λ, |K (σ i) τ| - 1

Injective indexing bounds the row sum away from the diagonal by the full sum minus one.

theorem LongGapsBetweenPrimes.indexed_product_second_moment {α : Type u_1} {ι : Type u_2} [Fintype α] [DecidableEq α] [Fintype ι] (size : α → ℕ) (hsize : ∀ (p : α), 1 < size p) {k : ℕ} (root : (p : α) → Fin k → Fin (size p)) (hroot : ∀ (p : α), Function.Injective (root p)) (σ : ι → α → Option (Fin k)) (hσ : Function.Injective σ) (c : ι → ℝ) (ε : ℝ) (hbound : ∀ (i : ι), ∏ p : α, localRow (size p) k (σ i p) - 1 ≤ ε) : |(Finset.univ.expect fun (t : (p : α) → Fin (size p)) => (∑ i : ι, c i * productBasis (fun (p : α) => localBasis (root p)) (σ i) t) ^ 2) - ∑ i : ι, c i ^ 2| ≤ ε * ∑ i : ι, c i ^ 2

Row bounds control the second moment of an indexed sum of product basis functions.

@[reducible, inline]

abbrev LongGapsBetweenPrimes.PrimeIndex (P : ℕ) : Type

Prime divisors of P regarded as a finite index type.

Equations

• LongGapsBetweenPrimes.PrimeIndex P = ↥P.primeFactors

noncomputable def LongGapsBetweenPrimes.tupleAssignment {P k : ℕ} (r : DivisorTuple P k) : PrimeIndex P → Option (Fin k)

Assign each used prime to a tuple coordinate containing it.

Equations

• LongGapsBetweenPrimes.tupleAssignment r p = if h : ∃ (i : Fin k), ↑p ∣ ↑(r i) then some (Classical.choose h) else none

theorem LongGapsBetweenPrimes.prime_coordinate_unique {P k p : ℕ} (hp : Nat.Prime p) (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) {i j : Fin k} (hi : p ∣ ↑(r i)) (hj : p ∣ ↑(r j)) : i = j

A prime divides at most one coordinate of a pairwise coprime tuple.

theorem LongGapsBetweenPrimes.tupleAssignment_eq_some {P k : ℕ} (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) (p : PrimeIndex P) (i : Fin k) : tupleAssignment r p = some i ↔ ↑p ∣ ↑(r i)

In a pairwise coprime tuple, a prime is assigned exactly to the coordinate it divides.

theorem LongGapsBetweenPrimes.tupleAssignment_injective {P k : ℕ} (hP : Squarefree P) (D : ℝ) : Function.Injective fun (r : ↥(tupleRegion P k D)) => tupleAssignment ↑r

A truncated tuple is determined by its prime assignment when P is squarefree.

theorem LongGapsBetweenPrimes.tupleAssignment_prod {P k : ℕ} {M : Type u_1} [CommMonoid M] (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) (f : PrimeIndex P → Fin k → M) : (∏ p : PrimeIndex P, match tupleAssignment r p with | none => 1 | some i => f p i) = ∏ i : Fin k, ∏ p : PrimeIndex P, if ↑p ∣ ↑(r i) then f p i else 1

Regroup a product over assigned primes by tuple coordinates.

theorem LongGapsBetweenPrimes.prod_primeIndex_dvd {P d : ℕ} (hP : P ≠ 0) (hd : d ∣ P) {M : Type u_1} [CommMonoid M] (f : ℕ → M) : (∏ p : PrimeIndex P, if ↑p ∣ d then f ↑p else 1) = ∏ p ∈ d.primeFactors, f p

Restrict a product over primes dividing P to those dividing d.

theorem LongGapsBetweenPrimes.tupleProduct_dvd {P k : ℕ} (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) : tupleProduct r ∣ P

The product of pairwise coprime divisors of P divides P.

theorem LongGapsBetweenPrimes.tupleAssignment_isSome {P k : ℕ} (r : DivisorTuple P k) (p : PrimeIndex P) : (tupleAssignment r p).isSome = true ↔ ↑p ∣ tupleProduct r

A prime is assigned precisely when it divides the tuple product.

theorem LongGapsBetweenPrimes.assignmentProduct_tupleAssignment {P k : ℕ} (hP : Squarefree P) (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) : assignmentProduct (fun (p : PrimeIndex P) => ↑p) (tupleAssignment r) = tupleProduct r

The product of assigned primes equals the tuple product for squarefree P.

noncomputable def LongGapsBetweenPrimes.rawLocalBasis {p k : ℕ} (root : Fin k → Fin p) (i : Option (Fin k)) (t : Fin p) : ℝ

The constant function and unnormalized residue factors.

Equations

• LongGapsBetweenPrimes.rawLocalBasis root none t = 1
• LongGapsBetweenPrimes.rawLocalBasis root (some j) t = LongGapsBetweenPrimes.residueFactor (root j) t

noncomputable def LongGapsBetweenPrimes.assignmentNormalizer {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ : α → Option (Fin k)) : ℝ

The factor converting normalized product basis functions to unnormalized ones.

Equations

• LongGapsBetweenPrimes.assignmentNormalizer size σ = ∏ p : α, match σ p with | none => 1 | some val => (√(↑(size p) - 1))⁻¹

noncomputable def LongGapsBetweenPrimes.assignmentVariance {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ : α → Option (Fin k)) : ℝ

The product of local variances on an assignment's support.

Equations

• LongGapsBetweenPrimes.assignmentVariance size σ = ∏ p : α, match σ p with | none => 1 | some val => 1 / (↑(size p) - 1)

theorem LongGapsBetweenPrimes.assignmentNormalizer_sq {α : Type u_1} [Fintype α] (size : α → ℕ) (hsize : ∀ (p : α), 1 < size p) {k : ℕ} (σ : α → Option (Fin k)) : assignmentNormalizer size σ ^ 2 = assignmentVariance size σ

The square of the assignment normalizer equals the assignment variance.

theorem LongGapsBetweenPrimes.assignmentNormalizer_mul_basis {α : Type u_1} [Fintype α] (size : α → ℕ) (hsize : ∀ (p : α), 1 < size p) {k : ℕ} (root : (p : α) → Fin k → Fin (size p)) (σ : α → Option (Fin k)) (t : (p : α) → Fin (size p)) : assignmentNormalizer size σ * productBasis (fun (p : α) => localBasis (root p)) σ t = productBasis (fun (p : α) => rawLocalBasis (root p)) σ t

Multiplying by the assignment normalizer removes the local basis normalization.

theorem LongGapsBetweenPrimes.prod_primeFactors_inv_sub_one {d : ℕ} (hd : Squarefree d) : ∏ p ∈ d.primeFactors, 1 / (↑p - 1) = 1 / ↑d.totient

For squarefree d, the product of 1 / (p - 1) equals 1 / φ(d).

theorem LongGapsBetweenPrimes.assignmentVariance_tuple {P k : ℕ} (hP : Squarefree P) (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) : assignmentVariance (fun (p : PrimeIndex P) => ↑p) (tupleAssignment r) = ∏ i : Fin k, 1 / ↑(↑(r i)).totient

A tuple's assignment variance is the product of its reciprocal totients.

noncomputable def LongGapsBetweenPrimes.tupleAmplitude {P k : ℕ} (r : DivisorTuple P k) : ℝ

The product of coefficients attached to a divisor tuple.

Equations

• LongGapsBetweenPrimes.tupleAmplitude r = ∏ i : Fin k, LongGapsBetweenPrimes.coefficient P ↑(r i)

noncomputable def LongGapsBetweenPrimes.tupleNormalizedCoefficient {P k : ℕ} (r : DivisorTuple P k) : ℝ

The tuple amplitude rescaled for expansion in the normalized basis.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.tupleNormalizedCoefficient_sq {P k : ℕ} (hP : Squarefree P) (r : DivisorTuple P k) (hpair : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) : tupleNormalizedCoefficient r ^ 2 = tupleMass r

A normalized tuple coefficient has square equal to its diagonal mass.

noncomputable def LongGapsBetweenPrimes.residueWeight (P k : ℕ) (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (t : (p : PrimeIndex P) → Fin ↑p) : ℝ

The truncated divisor sum weighted by coefficients and local residue factors.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.residueWeight_second_moment {P k : ℕ} (hP : Squarefree P) (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (ε : ℝ) (hbound : ∀ (r : ↥(tupleRegion P k D)), ∏ p : PrimeIndex P, localRow (↑p) k (tupleAssignment (↑r) p) - 1 ≤ ε) : |(Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => residueWeight P k D root t ^ 2) - diagonalMass P k D| ≤ ε * diagonalMass P k D

The tuple weight has the diagonal second moment claimed in (3.9).

theorem LongGapsBetweenPrimes.residueWeight_second_moment_bound {P k : ℕ} (hP : Squarefree P) (hk : 1 ≤ k) {M D : ℝ} (hM : 1 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) : |(Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => residueWeight P k D root t ^ 2) - diagonalMass P k D| ≤ (Real.exp (↑k * Real.log D / ((M - 1) * Real.log M)) - 1) * diagonalMass P k D

An explicit exponential bound for the second moment's deviation from the diagonal mass.

noncomputable def LongGapsBetweenPrimes.integerAverage (T : ℕ) (f : ℕ → ℝ) : ℝ

The average of f over the integers in [0, T).

Equations

• LongGapsBetweenPrimes.integerAverage T f = (∑ n ∈ Finset.range T, f n) / ↑T

theorem LongGapsBetweenPrimes.residue_expansion {m : ℕ} (hm : 0 < m) (g : Fin m → ℝ) (n : ℕ) : g ⟨n % m, ⋯⟩ = ∑ a : Fin m, g a * residueIndicator m (↑a) n

Expand a function of residues as a sum of residue indicators.

theorem LongGapsBetweenPrimes.integerAverage_residue_expansion {m : ℕ} (hm : 0 < m) (g : Fin m → ℝ) (T : ℕ) : (integerAverage T fun (n : ℕ) => g ⟨n % m, ⋯⟩) = ∑ a : Fin m, g a * ((∑ n ∈ Finset.range T, residueIndicator m (↑a) n) / ↑T)

Express a periodic average using the frequencies of its residue classes.

theorem LongGapsBetweenPrimes.residue_average_bounded_error {m T : ℕ} (hm : 0 < m) (hT : 0 < T) (g : Fin m → ℝ) (hg : ∀ (a : Fin m), |g a| ≤ 1) : |(integerAverage T fun (n : ℕ) => g ⟨n % m, ⋯⟩) - Finset.univ.expect g| ≤ ↑m / ↑T

A bounded function of one residue class has interval-average error at most m/T.

theorem LongGapsBetweenPrimes.integerAverage_complete_residues {m q : ℕ} (hm : 0 < m) (hq : 0 < q) (hmq : m ∣ q) (g : Fin m → ℝ) : (integerAverage q fun (n : ℕ) => g ⟨n % m, ⋯⟩) = Finset.univ.expect g

Averaging over complete periods equals the uniform average over residues.

theorem LongGapsBetweenPrimes.integerAverage_period_error {m q T : ℕ} (hm : 0 < m) (hq : 0 < q) (hT : 0 < T) (hmq : m ∣ q) (f : ℕ → ℝ) (hperiod : ∀ (n : ℕ), f (n % m) = f n) (hf : ∀ (n : ℕ), |f n| ≤ 1) : |integerAverage T f - integerAverage q f| ≤ ↑m / ↑T

The interval average of a bounded periodic function has error at most m / T.

theorem LongGapsBetweenPrimes.integerAverage_weight_sq {ι : Type u_1} [Fintype ι] (T : ℕ) (c : ι → ℝ) (f : ι → ℕ → ℝ) : (integerAverage T fun (n : ℕ) => (∑ i : ι, c i * f i n) ^ 2) = ∑ i : ι, ∑ j : ι, c i * c j * integerAverage T fun (n : ℕ) => f i n * f j n

Expand the average of a squared weighted sum into pairwise averages.

theorem LongGapsBetweenPrimes.integerAverage_weight_error {ι : Type u_1} [Fintype ι] (q T : ℕ) (c : ι → ℝ) (hc : ∀ (i : ι), |c i| ≤ 1) (f : ι → ℕ → ℝ) (E : ℝ) (hpair : ∀ (i j : ι), |(integerAverage T fun (n : ℕ) => f i n * f j n) - integerAverage q fun (n : ℕ) => f i n * f j n| ≤ E) : |(integerAverage T fun (n : ℕ) => (∑ i : ι, c i * f i n) ^ 2) - integerAverage q fun (n : ℕ) => (∑ i : ι, c i * f i n) ^ 2| ≤ ↑(Fintype.card ι) ^ 2 * E

Pairwise average errors give a quadratic error bound for a squared weighted sum.

def LongGapsBetweenPrimes.assignmentPrimes {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : Finset ℕ

The primes in the support of an assignment.

Equations

• LongGapsBetweenPrimes.assignmentPrimes σ = Finset.image Subtype.val (LongGapsBetweenPrimes.assignmentSupport σ)

theorem LongGapsBetweenPrimes.assignmentPrimes_subset {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : assignmentPrimes σ ⊆ P.primeFactors

Every assigned prime divides P.

theorem LongGapsBetweenPrimes.mem_assignmentPrimes {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) (p : PrimeIndex P) : ↑p ∈ assignmentPrimes σ ↔ (σ p).isSome = true

A prime belongs to the assigned set exactly when its assignment is nonempty.

theorem LongGapsBetweenPrimes.assignmentPrimes_prime {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) {p : ℕ} (hp : p ∈ assignmentPrimes σ) : Nat.Prime p

Every element of the assigned prime set is prime.

theorem LongGapsBetweenPrimes.assignmentPrimes_product {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : ∏ p ∈ assignmentPrimes σ, p = assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ

The product of the assigned primes equals the assignment product.

theorem LongGapsBetweenPrimes.assignmentProduct_pos {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : 0 < assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ

The product of the assigned primes is positive.

theorem LongGapsBetweenPrimes.assignmentProduct_dvd {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ ∣ P

The product of the assigned primes divides P.

theorem LongGapsBetweenPrimes.assignmentProduct_primeFactors {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) : (assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ).primeFactors = assignmentPrimes σ

The prime factors of the assignment product are exactly the assigned primes.

def LongGapsBetweenPrimes.assignedRoot {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (σ : PrimeIndex P → Option (Fin k)) (p : PrimeIndex P) : Fin ↑p

The root selected by an assignment, with zero at unused primes.

Equations

• LongGapsBetweenPrimes.assignedRoot root σ p = match σ p with | none => ⟨0, ⋯⟩ | some i => root p i

theorem LongGapsBetweenPrimes.exists_assignment_residue {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (σ : PrimeIndex P → Option (Fin k)) : ∃ a < assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ, ∀ (p : PrimeIndex P), (σ p).isSome = true → a % ↑p = ↑(assignedRoot root σ p)

The Chinese remainder theorem realizes all assigned roots in one residue.

noncomputable def LongGapsBetweenPrimes.assignmentCode {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (σ : PrimeIndex P → Option (Fin k)) : ℕ

A residue encoding the roots selected by an assignment.

Equations

• LongGapsBetweenPrimes.assignmentCode root σ = Classical.choose ⋯

theorem LongGapsBetweenPrimes.assignmentCode_lt {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (σ : PrimeIndex P → Option (Fin k)) : assignmentCode root σ < assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ

The assignment code is smaller than its modulus.

theorem LongGapsBetweenPrimes.assignmentCode_mod {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (σ : PrimeIndex P → Option (Fin k)) (p : PrimeIndex P) (hp : (σ p).isSome = true) : assignmentCode root σ % ↑p = ↑(assignedRoot root σ p)

The assignment code has the prescribed residue at each assigned prime.

theorem LongGapsBetweenPrimes.assignmentCode_determines {P k : ℕ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (σ τ : PrimeIndex P → Option (Fin k)) (hn : assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ = assignmentProduct (fun (p : PrimeIndex P) => ↑p) τ) (ha : assignmentCode root σ = assignmentCode root τ) : σ = τ

Distinct local roots make the modulus and residue code determine the assignment.

theorem LongGapsBetweenPrimes.card_assignment_family_le {P k : ℕ} {ι : Type u_1} [Fintype ι] (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (σ : ι → PrimeIndex P → Option (Fin k)) (hσ : Function.Injective σ) {D : ℝ} (hD : 1 ≤ D) (hcut : ∀ (i : ι), ↑(assignmentProduct (fun (p : PrimeIndex P) => ↑p) (σ i)) ≤ D) : ↑(Fintype.card ι) ≤ 4 * D ^ 2

Encoding an assignment by its modulus and one CRT residue bounds its count.

theorem LongGapsBetweenPrimes.tupleRegion_card_le {P k : ℕ} (hP : Squarefree P) {D : ℝ} (hD : 1 ≤ D) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) : ↑(Fintype.card ↥(tupleRegion P k D)) ≤ 4 * D ^ 2

The truncated tuple region has at most 4 * D ^ 2 elements.

theorem LongGapsBetweenPrimes.mod_invariant_of_dvd {m n : ℕ} (hmn : m ∣ n) (f : ℕ → ℝ) (hf : ∀ (a : ℕ), f (a % m) = f a) (a : ℕ) : f (a % n) = f a

Invariance modulo m implies invariance modulo every multiple of m.

theorem LongGapsBetweenPrimes.integerAverage_bounded_periodic_weight {ι : Type u_1} [Fintype ι] {q T : ℕ} (hq : 0 < q) (hT : 0 < T) {D : ℝ} (hD : 0 ≤ D) (period : ι → ℕ) (hperiod_pos : ∀ (i : ι), 0 < period i) (hperiod_q : ∀ (i : ι), period i ∣ q) (hperiod_D : ∀ (i : ι), ↑(period i) ≤ D) (c : ι → ℝ) (hc : ∀ (i : ι), |c i| ≤ 1) (f : ι → ℕ → ℝ) (hf : ∀ (i : ι) (n : ℕ), |f i n| ≤ 1) (hmod : ∀ (i : ι) (n : ℕ), f i (n % period i) = f i n) : |(integerAverage T fun (n : ℕ) => (∑ i : ι, c i * f i n) ^ 2) - integerAverage q fun (n : ℕ) => (∑ i : ι, c i * f i n) ^ 2| ≤ ↑(Fintype.card ι) ^ 2 * (D ^ 2 / ↑T)

Bound the second-moment averaging error using the periods and number of summands.

def LongGapsBetweenPrimes.residueVector (P n : ℕ) (p : PrimeIndex P) : Fin ↑p

The residues of n modulo the prime divisors of P.

Equations

• LongGapsBetweenPrimes.residueVector P n p = ⟨n % ↑p, ⋯⟩

theorem LongGapsBetweenPrimes.integerAverage_residues {P : ℕ} (hP : Squarefree P) (f : ((p : PrimeIndex P) → Fin ↑p) → ℝ) : (integerAverage P fun (n : ℕ) => f (residueVector P n)) = Finset.univ.expect f

The Chinese remainder theorem identifies a full-period average with a product average.

theorem LongGapsBetweenPrimes.abs_residueFactor_le_one {p : ℕ} (hp : 1 < p) (a t : Fin p) : |residueFactor a t| ≤ 1

Every residue factor has absolute value at most one.

theorem LongGapsBetweenPrimes.abs_rawLocalBasis_le_one {p k : ℕ} (hp : 1 < p) (root : Fin k → Fin p) (i : Option (Fin k)) (t : Fin p) : |rawLocalBasis root i t| ≤ 1

Every unnormalized local basis value has absolute value at most one.

theorem LongGapsBetweenPrimes.abs_productBasis_le_one {α : Type u_1} [Fintype α] {Ω : α → Type u_2} {J : α → Type u_3} (f : (p : α) → J p → Ω p → ℝ) (hf : ∀ (p : α) (i : J p) (t : Ω p), |f p i t| ≤ 1) (σ : (p : α) → J p) (t : (p : α) → Ω p) : |productBasis f σ t| ≤ 1

A product of local basis values bounded by one is bounded by one.

theorem LongGapsBetweenPrimes.tupleAmplitude_abs_le {P k : ℕ} (h : ∀ d ∈ P.divisors, |coefficient P d| ≤ 1) (r : DivisorTuple P k) : |tupleAmplitude r| ≤ 1

Coefficients bounded by one give tuple amplitudes bounded by one.

theorem LongGapsBetweenPrimes.prime_dvd_assignmentProduct {P k : ℕ} (σ : PrimeIndex P → Option (Fin k)) (p : PrimeIndex P) (hp : (σ p).isSome = true) : ↑p ∣ assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ

Every assigned prime divides the assignment product.

theorem LongGapsBetweenPrimes.basisProduct_mod_invariant {P k : ℕ} (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (hf : ∀ (p : PrimeIndex P) (t : Fin ↑p), f p none t = 1) (σ : PrimeIndex P → Option (Fin k)) (n : ℕ) : productBasis f σ (residueVector P (n % assignmentProduct (fun (p : PrimeIndex P) => ↑p) σ)) = productBasis f σ (residueVector P n)

A product basis function depends only on the residue modulo its assignment product.

noncomputable def LongGapsBetweenPrimes.basisWeight (P k : ℕ) (D : ℝ) (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (t : (p : PrimeIndex P) → Fin ↑p) : ℝ

The truncated tuple sum formed from an arbitrary family of local basis functions.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.basisWeight_interval_error {P k T : ℕ} (hP : Squarefree P) (hT : 0 < T) {D : ℝ} (hD : 1 ≤ D) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (hcoeff : ∀ d ∈ P.divisors, |coefficient P d| ≤ 1) (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (hfnone : ∀ (p : PrimeIndex P) (t : Fin ↑p), f p none t = 1) (hf : ∀ (p : PrimeIndex P) (i : Option (Fin k)) (t : Fin ↑p), |f p i t| ≤ 1) : |(integerAverage T fun (n : ℕ) => basisWeight P k D f (residueVector P n) ^ 2) - Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => basisWeight P k D f t ^ 2| ≤ 16 * D ^ 6 / ↑T

A D^6/T error is sufficient after taking κ = 1/8 in the final parameter choice.

theorem LongGapsBetweenPrimes.residueWeight_interval_error {P k T : ℕ} (hP : Squarefree P) (hT : 0 < T) {D : ℝ} (hD : 1 ≤ D) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (hcoeff : ∀ d ∈ P.divisors, |coefficient P d| ≤ 1) : |(integerAverage T fun (n : ℕ) => residueWeight P k D root (residueVector P n) ^ 2) - Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => residueWeight P k D root t ^ 2| ≤ 16 * D ^ 6 / ↑T

The residue weight's second-moment averaging error is at most 16 * D ^ 6 / T.

theorem LongGapsBetweenPrimes.tupleProduct_pos {P k : ℕ} (r : DivisorTuple P k) : 0 < tupleProduct r

Every divisor tuple has positive product.

theorem LongGapsBetweenPrimes.tupleProduct_insertNth {P k : ℕ} (i : Fin (k + 1)) (d : DivisorIndex P) (r : DivisorTuple P k) : tupleProduct (i.insertNth d r) = ↑d * tupleProduct r

Inserting a divisor multiplies the tuple product by that divisor.

theorem LongGapsBetweenPrimes.tuplePairwise_insertNth {P k : ℕ} (i : Fin (k + 1)) (d : DivisorIndex P) (r : DivisorTuple P k) : (∀ (j l : Fin (k + 1)), j ≠ l → (↑(i.insertNth d r j)).Coprime ↑(i.insertNth d r l)) ↔ (∀ (j l : Fin k), j ≠ l → (↑(r j)).Coprime ↑(r l)) ∧ (↑d).Coprime (tupleProduct r)

Insertion preserves pairwise coprimality iff the new divisor is coprime to the rest.

theorem LongGapsBetweenPrimes.tupleRegion_insertNth {P k : ℕ} (i : Fin (k + 1)) (d : DivisorIndex P) (r : DivisorTuple P k) (D : ℝ) : i.insertNth d r ∈ tupleRegion P (k + 1) D ↔ r ∈ tupleRegion P k D ∧ ↑↑d ≤ D / ↑(tupleProduct r) ∧ (↑d).Coprime (tupleProduct r)

Characterize truncated-region membership after inserting one divisor.

theorem LongGapsBetweenPrimes.tupleSum_split {P k : ℕ} (i : Fin (k + 1)) (D : ℝ) (G : Fin (k + 1) → DivisorIndex P → ℝ) : ∑ r ∈ tupleRegion P (k + 1) D, ∏ j : Fin (k + 1), G j (r j) = ∑ r ∈ tupleRegion P k D, (∑ d : DivisorIndex P, if ↑↑d ≤ D / ↑(tupleProduct r) ∧ (↑d).Coprime (tupleProduct r) then G i d else 0) * ∏ j : Fin k, G (i.succAbove j) (r j)

Split a truncated tuple sum by one coordinate.

noncomputable def LongGapsBetweenPrimes.coefficientRemainder (P m : ℕ) (D : ℝ) : ℝ

The partial coefficient sum over small divisors coprime to m.

Equations

• LongGapsBetweenPrimes.coefficientRemainder P m D = ∑ d ∈ P.divisors with ↑d ≤ D / ↑m ∧ d.Coprime m, LongGapsBetweenPrimes.coefficient P d / ↑d.totient

theorem LongGapsBetweenPrimes.coefficientRemainder_eq_sum (P m : ℕ) (D : ℝ) : coefficientRemainder P m D = ∑ d : DivisorIndex P, if ↑↑d ≤ D / ↑m ∧ (↑d).Coprime m then coefficient P ↑d / ↑(↑d).totient else 0

Express the coefficient remainder as a sum over divisor indices.

def LongGapsBetweenPrimes.coordinateBasis {P k : ℕ} (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (d : DivisorIndex P) (i : Fin k) (t : (p : PrimeIndex P) → Fin ↑p) : ℝ

The local basis product for one divisor and tuple coordinate.

Equations

• LongGapsBetweenPrimes.coordinateBasis f d i t = ∏ p : LongGapsBetweenPrimes.PrimeIndex P, if ↑p ∣ ↑d then f p (some i) (t p) else 1

theorem LongGapsBetweenPrimes.productBasis_tupleAssignment {P k : ℕ} (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (hf : ∀ (p : PrimeIndex P) (t : Fin ↑p), f p none t = 1) (r : DivisorTuple P k) (hr : ∀ (i j : Fin k), i ≠ j → (↑(r i)).Coprime ↑(r j)) (t : (p : PrimeIndex P) → Fin ↑p) : productBasis f (tupleAssignment r) t = ∏ i : Fin k, coordinateBasis f (r i) i t

Factor a tuple's product basis function over its coordinates.

theorem LongGapsBetweenPrimes.basisWeight_eq_tupleSum {P k : ℕ} (D : ℝ) (f : (p : PrimeIndex P) → Option (Fin k) → Fin ↑p → ℝ) (hf : ∀ (p : PrimeIndex P) (t : Fin ↑p), f p none t = 1) (t : (p : PrimeIndex P) → Fin ↑p) : basisWeight P k D f t = ∑ r ∈ tupleRegion P k D, ∏ i : Fin k, coefficient P ↑(r i) * coordinateBasis f (r i) i t

Expand a basis weight as a sum of products over tuple coordinates.

noncomputable def LongGapsBetweenPrimes.replacedLocalBasis {p k : ℕ} (root : Fin k → Fin p) (i : Fin k) (j : Option (Fin k)) (t : Fin p) : ℝ

The local basis with coordinate i replaced by the constant 1 / (p - 1).

Equations

• LongGapsBetweenPrimes.replacedLocalBasis root i none t = 1
• LongGapsBetweenPrimes.replacedLocalBasis root i (some j_1) t = if j_1 = i then 1 / (↑p - 1) else LongGapsBetweenPrimes.residueFactor (root j_1) t

theorem LongGapsBetweenPrimes.coordinateBasis_replaced {P k : ℕ} (hP : Squarefree P) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (i j : Fin k) (d : DivisorIndex P) (t : (p : PrimeIndex P) → Fin ↑p) : coordinateBasis (fun (p : PrimeIndex P) => replacedLocalBasis (root p) i) d j t = if j = i then 1 / ↑(↑d).totient else coordinateBasis (fun (p : PrimeIndex P) => rawLocalBasis (root p)) d j t

Replacing a coordinate reduces its divisor basis factor to the reciprocal totient.

noncomputable def LongGapsBetweenPrimes.replacedResidueWeight (P k : ℕ) (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (i : Fin k) (t : (p : PrimeIndex P) → Fin ↑p) : ℝ

The residue weight with one marked coordinate replaced by constants.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.replacedResidueWeight_split {P k : ℕ} (hP : Squarefree P) (D : ℝ) (root : (p : PrimeIndex P) → Fin (k + 1) → Fin ↑p) (i : Fin (k + 1)) (t : (p : PrimeIndex P) → Fin ↑p) : replacedResidueWeight P (k + 1) D root i t = ∑ r ∈ tupleRegion P k D, coefficientRemainder P (tupleProduct r) D * ∏ j : Fin k, coefficient P ↑(r j) * coordinateBasis (fun (p : PrimeIndex P) => rawLocalBasis fun (j : Fin k) => root p (i.succAbove j)) (r j) j t

Split the replaced weight into smaller tuples and coefficient remainders.

theorem LongGapsBetweenPrimes.coefficient_noncoprime_le {P m : ℕ} (hP : 1 < P) (hsq : Squarefree P) (hm : m ∣ P) (hcoeff : ∀ d ∈ P.divisors, |coefficient P d| ≤ 1) : ∑ d ∈ P.divisors with ¬d.Coprime m, |coefficient P d| / ↑d.totient ≤ ∑ p ∈ m.primeFactors, 4 / ↑p

Bound the coefficient mass of divisors sharing a prime with m by a prime sum.

theorem LongGapsBetweenPrimes.sum_primeFactors_inv_le {P m : ℕ} (hP : Squarefree P) (hm : m ∣ P) {M : ℝ} (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) : ∑ p ∈ m.primeFactors, 4 / ↑p ≤ 4 * Real.log ↑m / (M * Real.log 2)

A lower bound on prime factors controls their reciprocal sum using log m.

theorem LongGapsBetweenPrimes.coefficientRemainder_nonneg {P m : ℕ} (hP : 1 < P) (hm : 0 < m) {D : ℝ} (hcut : ↑m ≤ D) : 0 ≤ coefficientRemainder P m D

The coefficient remainder is nonnegative when its cutoff includes one.

theorem LongGapsBetweenPrimes.coefficient_tail_le {P : ℕ} {v β : ℝ} (hv : 1 ≤ v) (hβ : 0 ≤ β) : ∑ d ∈ P.divisors with v < ↑d, |coefficient P d| / ↑d.totient ≤ v ^ (-β) * coefficientAbsMoment P β

Rankin's bound for the absolute coefficient tail.

theorem LongGapsBetweenPrimes.coefficientRemainder_le_tail_add_overlap {P m : ℕ} (hP : 1 < P) (hm : 0 < m) {D : ℝ} (hcut : ↑m ≤ D) : coefficientRemainder P m D ≤ ∑ d ∈ P.divisors with D / ↑m < ↑d, |coefficient P d| / ↑d.totient + ∑ d ∈ P.divisors with ¬d.Coprime m, |coefficient P d| / ↑d.totient

Bound the coefficient remainder by the discarded tail and noncoprime mass.

theorem LongGapsBetweenPrimes.coefficientRemainder_le {P m : ℕ} {β C D M : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hm : m ∣ P) (hcut : ↑m ≤ D) (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) : coefficientRemainder P m D ≤ C * (↑m / D) ^ β + 4 * Real.log D / (M * Real.log 2)

Bound the coefficient remainder by a power tail and an error from shared primes.

theorem LongGapsBetweenPrimes.assignment_row_bound_all {α : Type u_1} [Fintype α] (size : α → ℕ) {k : ℕ} (σ : α → Option (Fin k)) {M D : ℝ} (hM : 1 < M) (hsize : ∀ (p : α), M ≤ ↑(size p)) (hcut : ↑(assignmentProduct size σ) ≤ D) : ∏ p : α, localRow (size p) k (σ p) ≤ Real.exp (↑k * Real.log D / ((M - 1) * Real.log M))

An exponential assignment row bound valid for every tuple length.

noncomputable def LongGapsBetweenPrimes.weightedResidueWeight (P k : ℕ) (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (b : DivisorTuple P k → ℝ) (t : (p : PrimeIndex P) → Fin ↑p) : ℝ

The residue weight with an additional weight on each divisor tuple.

Equations

• One or more equations did not get rendered due to their size.

theorem LongGapsBetweenPrimes.weightedResidueWeight_eq_sum {P k : ℕ} (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (b : DivisorTuple P k → ℝ) (t : (p : PrimeIndex P) → Fin ↑p) : weightedResidueWeight P k D root b t = ∑ r ∈ tupleRegion P k D, b r * ∏ i : Fin k, coefficient P ↑(r i) * coordinateBasis (fun (p : PrimeIndex P) => rawLocalBasis (root p)) (r i) i t

Expand the weighted residue sum as a product over tuple coordinates.

theorem LongGapsBetweenPrimes.weightedResidueWeight_second_moment_le {P k : ℕ} (hP : Squarefree P) {D M : ℝ} (hM : 1 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (b : DivisorTuple P k → ℝ) : (Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => weightedResidueWeight P k D root b t ^ 2) ≤ Real.exp (↑k * Real.log D / ((M - 1) * Real.log M)) * ∑ r ∈ tupleRegion P k D, tupleMass r * b r ^ 2

Bound the weighted second moment by the Gram factor times its diagonal mass.

theorem LongGapsBetweenPrimes.replacedResidueWeight_eq_weighted {P k : ℕ} (hP : Squarefree P) (D : ℝ) (root : (p : PrimeIndex P) → Fin (k + 1) → Fin ↑p) (i : Fin (k + 1)) (t : (p : PrimeIndex P) → Fin ↑p) : replacedResidueWeight P (k + 1) D root i t = weightedResidueWeight P k D (fun (p : PrimeIndex P) (j : Fin k) => root p (i.succAbove j)) (fun (r : DivisorTuple P k) => coefficientRemainder P (tupleProduct r) D) t

A replaced weight is a weight on smaller tuples with coefficient-remainder factors.

theorem LongGapsBetweenPrimes.weighted_diagonal_le {P k : ℕ} {D a b γ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (v : DivisorTuple P k → ℝ) (hv : ∀ r ∈ tupleRegion P k D, v r ^ 2 ≤ a * ↑(tupleProduct r) ^ γ + b) : ∑ r ∈ tupleRegion P k D, tupleMass r * v r ^ 2 ≤ a * coefficientMoment P γ ^ k + b * coefficientMoment P 0 ^ k

Control weighted diagonal mass by tilted and zero coefficient moments.

theorem LongGapsBetweenPrimes.coefficientRemainder_square_le {P m : ℕ} {β C D M : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hm : m ∣ P) (hcut : ↑m ≤ D) (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) : coefficientRemainder P m D ^ 2 ≤ 2 * C ^ 2 * D ^ (-(2 * β)) * ↑m ^ (2 * β) + 2 * (4 * Real.log D / (M * Real.log 2)) ^ 2

Bound the squared coefficient remainder by its tail and overlap contributions.

theorem LongGapsBetweenPrimes.replacedResidueWeight_second_moment_le {P k : ℕ} {β C D M : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hD : 0 < D) (hM : 1 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) (root : (p : PrimeIndex P) → Fin (k + 1) → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (i : Fin (k + 1)) : (Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => replacedResidueWeight P (k + 1) D root i t ^ 2) ≤ Real.exp (↑k * Real.log D / ((M - 1) * Real.log M)) * (2 * C ^ 2 * D ^ (-(2 * β)) * coefficientMoment P (2 * β) ^ k + 2 * (4 * Real.log D / (M * Real.log 2)) ^ 2 * coefficientMoment P 0 ^ k)

Bound a replaced weight's second moment using tilted and zero coefficient moments.

theorem LongGapsBetweenPrimes.residueWeight_eq_replaced_of_uncovered {P k : ℕ} (D : ℝ) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (i : Fin k) (t : (p : PrimeIndex P) → Fin ↑p) (hi : ∀ (p : PrimeIndex P), t p ≠ root p i) : residueWeight P k D root t = replacedResidueWeight P k D root i t

Avoiding one coordinate's roots makes the original and replaced weights equal.

theorem LongGapsBetweenPrimes.abs_replacedLocalBasis_le_one {p k : ℕ} (hp : 1 < p) (root : Fin k → Fin p) (i : Fin k) (j : Option (Fin k)) (t : Fin p) : |replacedLocalBasis root i j t| ≤ 1

Every replaced local basis value has absolute value at most one.

theorem LongGapsBetweenPrimes.replacedResidueWeight_interval_error {P k T : ℕ} (hP : Squarefree P) (hT : 0 < T) {D : ℝ} (hD : 1 ≤ D) (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (hcoeff : ∀ d ∈ P.divisors, |coefficient P d| ≤ 1) (i : Fin k) : |(integerAverage T fun (n : ℕ) => replacedResidueWeight P k D root i (residueVector P n) ^ 2) - Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => replacedResidueWeight P k D root i t ^ 2| ≤ 16 * D ^ 6 / ↑T

The replaced weight's second-moment averaging error is at most 16 * D ^ 6 / T.

theorem LongGapsBetweenPrimes.exists_simultaneous_root_of_moments {P k T : ℕ} {D L U : ℝ} (root : (p : PrimeIndex P) → Fin k → Fin ↑p) (hlower : L ≤ integerAverage T fun (n : ℕ) => residueWeight P k D root (residueVector P n) ^ 2) (hupper : ∀ (i : Fin k), (integerAverage T fun (n : ℕ) => replacedResidueWeight P k D root i (residueVector P n) ^ 2) ≤ U) (hgap : ↑k * U < L) : ∃ n < T, ∀ (i : Fin k), ∃ (p : PrimeIndex P), residueVector P n p = root p i

A second-moment gap yields an integer meeting a root in every coordinate.

theorem LongGapsBetweenPrimes.CoefficientEstimates.one_le_constant {P : ℕ} {β C : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) : 1 ≤ C

Any coefficient-estimate constant is at least one.

noncomputable def LongGapsBetweenPrimes.gramBound (k : ℕ) (M D : ℝ) : ℝ

The exponential factor controlling Gram matrix row sums.

Equations

• LongGapsBetweenPrimes.gramBound k M D = Real.exp (↑k * Real.log D / ((M - 1) * Real.log M))

noncomputable def LongGapsBetweenPrimes.uncoveredBound (k : ℕ) (β C M D : ℝ) : ℝ

A normalized second-moment bound for a replaced residue weight.

Equations

• LongGapsBetweenPrimes.uncoveredBound k β C M D = LongGapsBetweenPrimes.gramBound k M D * (2 * C ^ 2 * D ^ (-(2 * β)) * Real.exp (↑k * C * (2 * β)) + 2 * (4 * Real.log D / (M * Real.log 2)) ^ 2)

theorem LongGapsBetweenPrimes.uncoveredBound_nonneg (k : ℕ) (β C M : ℝ) {D : ℝ} (hD : 0 ≤ D) : 0 ≤ uncoveredBound k β C M D

The normalized uncovered bound is nonnegative.

theorem LongGapsBetweenPrimes.replacedResidueWeight_normalized_bound {P k : ℕ} {β C D M : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hD : 0 < D) (hM : 1 < M) (hmin : ∀ p ∈ P.primeFactors, M ≤ ↑p) (root : (p : PrimeIndex P) → Fin (k + 1) → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (i : Fin (k + 1)) : (Finset.univ.expect fun (t : (p : PrimeIndex P) → Fin ↑p) => replacedResidueWeight P (k + 1) D root i t ^ 2) ≤ uncoveredBound k β C M D * coefficientMoment P 0 ^ k

Bound a replaced weight's second moment by uncoveredBound times the zero moment.

theorem LongGapsBetweenPrimes.diagonalMass_normalized_lower {P M k : ℕ} {β C D : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hD : 0 < D) (hM : 0 < M) (hmin : ∀ p ∈ P.primeFactors, M < p) : (1 - (D ^ (-β) * Real.exp (↑k * C * β) + 16 * ↑k ^ 2 / ↑M)) * coefficientMoment P 0 ^ k ≤ diagonalMass P k D

The normalized diagonal mass loses only a power tail and prime collisions.

theorem LongGapsBetweenPrimes.finite_simultaneous_roots {P M k T : ℕ} {β C D : ℝ} (h : CoefficientEstimates P β C) (hβ : 0 ≤ β) (hD : 1 ≤ D) (hM : 1 < M) (hT : 0 < T) (hmin : ∀ p ∈ P.primeFactors, M < p) (root : (p : PrimeIndex P) → Fin (k + 1) → Fin ↑p) (hroot : ∀ (p : PrimeIndex P), Function.Injective (root p)) (htail : D ^ (-β) * Real.exp (↑(k + 1) * C * β) + 16 * ↑(k + 1) ^ 2 / ↑M ≤ 1 / 2) (hgram : gramBound (k + 1) (↑M) D ≤ 5 / 4) (herr : 16 * D ^ 6 / ↑T ≤ 1 / 8) (hbad : ↑(k + 1) * (uncoveredBound k β C (↑M) D + 16 * D ^ 6 / ↑T) < 1 / 4) : ∃ n < T, ∀ (i : Fin (k + 1)), ∃ (p : PrimeIndex P), residueVector P n p = root p i

The finite weighted sieve, with every numerical loss displayed explicitly.

noncomputable def LongGapsBetweenPrimes.sieveD (x : ℝ) : ℝ

The divisor-product cutoff exp (x / 8).

Equations

• LongGapsBetweenPrimes.sieveD x = Real.exp (x / 8)

noncomputable def LongGapsBetweenPrimes.sieveT (x : ℝ) : ℕ

The averaging interval length, given by the integer part of exp x.

Equations

• LongGapsBetweenPrimes.sieveT x = ⌊Real.exp x⌋₊

theorem LongGapsBetweenPrimes.exp_neg_nat_mul_log {x : ℝ} (hx : 0 < x) (n : ℕ) : Real.exp (-↑n * Real.log x) = 1 / x ^ n

Rewrite exp (-n * log x) as 1 / x ^ n.

theorem LongGapsBetweenPrimes.truncated_exponential_le {n : ℕ} {x β C : ℝ} (hx : 0 < x) (hβ : 0 ≤ β) (hsize : ↑n * C ≤ x / 16) (hlog : 48 * Real.log x ≤ x * β) : sieveD x ^ (-β) * Real.exp (↑n * C * β) ≤ 1 / x ^ 3

The truncation tail is at most 1 / x ^ 3 under the sieve size bounds.

theorem LongGapsBetweenPrimes.truncated_double_exponential_le {n : ℕ} {x β C : ℝ} (hx : 0 < x) (hβ : 0 ≤ β) (hsize : ↑n * C ≤ x / 16) (hlog : 48 * Real.log x ≤ x * β) : sieveD x ^ (-(2 * β)) * Real.exp (↑n * C * (2 * β)) ≤ 1 / x ^ 6

The truncation tail with doubled exponent is at most 1 / x ^ 6.

theorem LongGapsBetweenPrimes.gramBound_le_simple {n : ℕ} {M x : ℝ} (hx : 1 ≤ x) (hn : ↑n ≤ x) (hM : x ^ 4 ≤ M - 1) (hlog : 1 ≤ Real.log M) : gramBound n M (sieveD x) ≤ Real.exp (1 / x ^ 2)

Bound the Gram factor by exp (1 / x ^ 2).

theorem LongGapsBetweenPrimes.collisionBound_le_simple {n : ℕ} {M x : ℝ} (hx : 0 < x) (hn : ↑n ≤ x) (hM : x ^ 4 ≤ M) : 16 * ↑n ^ 2 / M ≤ 16 / x ^ 2

The collision contribution is at most 16 / x ^ 2.

theorem LongGapsBetweenPrimes.overlapBound_le_simple {M x : ℝ} (hx : 0 < x) (hM : x ^ 4 ≤ M) : 4 * Real.log (sieveD x) / (M * Real.log 2) ≤ 1 / (Real.log 2 * x ^ 3)

The overlap contribution is at most 1 / (log 2 * x ^ 3).

theorem LongGapsBetweenPrimes.uncoveredBound_le_simple {n : ℕ} {M x β C : ℝ} (hx : 1 ≤ x) (hβ : 0 ≤ β) (hn : ↑n ≤ x) (hsize : ↑n * C ≤ x / 16) (hlog : 48 * Real.log x ≤ x * β) (hM : x ^ 4 ≤ M - 1) (hlogM : 1 ≤ Real.log M) (hgram : Real.exp (1 / x ^ 2) ≤ 5 / 4) : uncoveredBound n β C M (sieveD x) ≤ 5 / 4 * (2 * C ^ 2 + 2 / Real.log 2 ^ 2) / x ^ 6

Bound the normalized uncovered contribution by an explicit multiple of 1 / x ^ 6.

theorem LongGapsBetweenPrimes.sieveZ_lower {x : ℝ} (hx : 2 ≤ x) : x ^ 4 ≤ ↑(sieveZ x) - 1

For x ≥ 2, the lower sieve cutoff exceeds x ^ 4 by at least one.

theorem LongGapsBetweenPrimes.sieveT_lower {x : ℝ} (hx : 2 ≤ x) : Real.exp x / 2 ≤ ↑(sieveT x)

The integer averaging length is at least half of exp x.

theorem LongGapsBetweenPrimes.intervalError_le_simple {x : ℝ} (hx : 2 ≤ x) (hlog : 12 * Real.log x ≤ x) : 16 * sieveD x ^ 6 / ↑(sieveT x) ≤ 32 / x ^ 3

The interval averaging error is at most 32 / x ^ 3.

theorem LongGapsBetweenPrimes.eventually_sieve_beta_scale : ∀ᶠ (x : ℝ) in Filter.atTop, 48 * Real.log x ≤ x * sieveBeta x

The sieve tilt eventually satisfies 48 * log x ≤ x * sieveBeta x.

theorem LongGapsBetweenPrimes.eventually_simple_sieve_bounds (C : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, Real.exp (1 / x ^ 2) ≤ 5 / 4 ∧ 1 / x ^ 3 + 16 / x ^ 2 ≤ 1 / 2 ∧ 32 / x ^ 3 ≤ 1 / 8 ∧ 5 / 4 * (2 * C ^ 2 + 2 / Real.log 2 ^ 2) / x ^ 5 + 32 / x ^ 2 < 1 / 4

The numerical sieve error bounds hold for all sufficiently large x.

noncomputable def LongGapsBetweenPrimes.sieveDelta : ℝ

The density threshold for simultaneously hitting all root families.

Equations

• LongGapsBetweenPrimes.sieveDelta = 1 / (64 * LongGapsBetweenPrimes.weightConstant)

theorem LongGapsBetweenPrimes.sieveDelta_pos : 0 < sieveDelta

The simultaneous-root density threshold is positive.

theorem LongGapsBetweenPrimes.sieveDelta_lt_half : sieveDelta < 1 / 2

The simultaneous-root density threshold is less than one half.

theorem LongGapsBetweenPrimes.eventually_simultaneous_roots : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (k : ℕ), ↑(k + 1) ≤ sieveDelta * x → ∀ (root : (p : PrimeIndex (sieveP x)) → Fin (k + 1) → Fin ↑p), (∀ (p : PrimeIndex (sieveP x)), Function.Injective (root p)) → ∃ n < sieveT x, ∀ (i : Fin (k + 1)), ∃ (p : PrimeIndex (sieveP x)), residueVector (sieveP x) n p = root p i

For large x, sufficiently small families of distinct roots can be hit simultaneously.

theorem LongGapsBetweenPrimes.eventually_sieveY_lt_primorial : ∀ᶠ (x : ℝ) in Filter.atTop, sieveY x < primorial ⌊x⌋₊

The upper sieve cutoff is eventually below the primorial up to x.

theorem LongGapsBetweenPrimes.exists_linear_roots {p k Q b : ℕ} (hp : Nat.Prime p) (hQ : Q.Coprime p) (s : Fin k → ℕ) (hs : Function.Injective s) (hsmall : ∀ (i : Fin k), s i < p) : ∃ (root : Fin k → Fin p), Function.Injective root ∧ ∀ (n : ℕ) (i : Fin k), n % p = ↑(root i) → p ∣ b + Q * (n + 1) + s i

Construct distinct modular roots forcing divisibility of the translated linear forms.

theorem LongGapsBetweenPrimes.short_translates_with_sieveDelta : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H : ℕ), x < ↑H → ↑H ≤ x * Real.log x ^ 2 → ∀ S ⊆ Finset.Icc 1 H, ↑S.card ≤ sieveDelta * x → ∀ b < primorial ⌊x⌋₊, ∃ (t : ℕ), 1 ≤ t ∧ ↑t ≤ Real.exp x ∧ ∀ s ∈ S, ¬Nat.Prime (b + primorial ⌊x⌋₊ * t + s)

Proposition 1.2, proved with the explicit coefficient construction above.

theorem LongGapsBetweenPrimes.short_translates : ShortTranslates

The sparse-set translation bound of Proposition 1.2.

noncomputable def LongGapsBetweenPrimes.smoothEulerConstant : ℝ

A uniform geometric factor for the smooth-number estimate.

Equations

• LongGapsBetweenPrimes.smoothEulerConstant = (1 - 2 ^ (-(1 / 2)))⁻¹

theorem LongGapsBetweenPrimes.smoothEulerConstant_pos : 0 < smoothEulerConstant

The smooth Euler constant is positive.

noncomputable def LongGapsBetweenPrimes.smoothScaleConstant : ℝ

The scale constant used to choose the smoothness cutoff and tilt.

Equations

• LongGapsBetweenPrimes.smoothScaleConstant = 3 * LongGapsBetweenPrimes.smoothEulerConstant + 10

theorem LongGapsBetweenPrimes.smoothScaleConstant_pos : 0 < smoothScaleConstant

The smoothness scale constant is positive.

theorem LongGapsBetweenPrimes.euler_factor_left_comparison {p t : ℝ} (hp : 2 ≤ p) (ht : 0 ≤ t) (ht' : t ≤ 1 / 2) : (1 - p ^ (-(1 - t)))⁻¹ ≤ (1 - p ^ (-1))⁻¹ * Real.exp (smoothEulerConstant * (p ^ t - 1) / p)

Bound the cost of shifting an Euler factor to exponent 1 - t.

theorem LongGapsBetweenPrimes.eulerProduct_left_comparison (N : ℕ) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1 / 2) : eulerProduct N (1 - t) ≤ eulerProduct N 1 * Real.exp (smoothEulerConstant * ∑ p ∈ N.primesLE, (↑p ^ t - 1) / ↑p)

Bound the cost of shifting the Euler product to exponent 1 - t.

theorem LongGapsBetweenPrimes.rpow_secant_log {p z t : ℝ} (hp : 1 ≤ p) (hpz : p ≤ z) (hz : 1 < z) (ht : 0 ≤ t) : p ^ t - 1 ≤ Real.log p / Real.log z * (Real.exp (t * Real.log z) - 1)

A secant bound controls p ^ t - 1 using the ratio log p / log z.

theorem LongGapsBetweenPrimes.eulerProduct_left_bound {N : ℕ} {z t : ℝ} (hN : 2 ≤ N) (hNz : ↑N ≤ z) (ht : 0 ≤ t) (ht' : t ≤ 1 / 2) : eulerProduct N (1 - t) ≤ eulerProduct N 1 * Real.exp (3 * smoothEulerConstant * Real.exp (t * Real.log z))

Bound the shifted Euler product using the tilt and the largest prime cutoff.

theorem LongGapsBetweenPrimes.smooth_count_rankin {N H : ℕ} {σ : ℝ} (hσ : 0 < σ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 H) (hsmooth : ∀ n ∈ S, n ∈ (N + 1).smoothNumbers) : ↑S.card ≤ ↑H ^ σ * eulerProduct N σ

A finite Euler-product bound for the count of smooth integers up to H.

noncomputable def LongGapsBetweenPrimes.coverLogZ (x : ℝ) : ℝ

The logarithmic smoothness cutoff in the covering construction.

Equations

• LongGapsBetweenPrimes.coverLogZ x = Real.log x * Real.log (Real.log (Real.log x)) / (LongGapsBetweenPrimes.smoothScaleConstant * Real.log (Real.log x))

noncomputable def LongGapsBetweenPrimes.coverZ (x : ℝ) : ℕ

The smoothness cutoff in the covering construction, rounded down to an integer.

Equations

• LongGapsBetweenPrimes.coverZ x = ⌊Real.exp (LongGapsBetweenPrimes.coverLogZ x)⌋₊

noncomputable def LongGapsBetweenPrimes.coverW (x : ℝ) : ℕ

The small-prime cutoff, given by the integer part of (log x)^4.

Equations

• LongGapsBetweenPrimes.coverW x = ⌊Real.log x ^ 4⌋₊

noncomputable def LongGapsBetweenPrimes.coverTilt (x : ℝ) : ℝ

The Rankin tilt used to count smooth integers.

Equations

• LongGapsBetweenPrimes.coverTilt x = LongGapsBetweenPrimes.smoothScaleConstant * Real.log (Real.log x) / Real.log x

noncomputable def LongGapsBetweenPrimes.coverLength (η x : ℝ) : ℕ

The integer interval length targeted by the covering argument.

Equations

• LongGapsBetweenPrimes.coverLength η x = ⌊η * x * Real.log x ^ 2 * Real.log (Real.log (Real.log x)) / Real.log (Real.log x) ^ 2⌋₊

theorem LongGapsBetweenPrimes.smoothScaleConstant_gt_ten : 10 < smoothScaleConstant

The smoothness scale constant exceeds ten.

theorem LongGapsBetweenPrimes.coverTilt_mul_coverLogZ {x : ℝ} (hx : 1 < x) (hlog : 1 < Real.log x) : coverTilt x * coverLogZ x = Real.log (Real.log (Real.log x))

The covering tilt times the logarithmic cutoff equals the third iterated logarithm.

theorem LongGapsBetweenPrimes.eventually_cover_parameters : ∀ᶠ (x : ℝ) in Filter.atTop, 2 ≤ x ∧ 2 ≤ Real.log x ∧ 1 ≤ Real.log (Real.log x) ∧ 1 ≤ Real.log (Real.log (Real.log x)) ∧ 4 * smoothScaleConstant * Real.log (Real.log x) ^ 2 ≤ Real.log x ∧ 0 ≤ coverTilt x ∧ coverTilt x ≤ 1 / 2 ∧ 4 * Real.log (Real.log x) ≤ coverLogZ x ∧ coverLogZ x ≤ Real.log x

The size, ordering, and tilt bounds for the covering parameters hold eventually.

theorem LongGapsBetweenPrimes.coverW_le_coverZ {x : ℝ} (hx : 1 < x) (hz : 4 * Real.log (Real.log x) ≤ coverLogZ x) : coverW x ≤ coverZ x

The small-prime cutoff does not exceed the smoothness cutoff.

theorem LongGapsBetweenPrimes.coverZ_le_floor {x : ℝ} (hx : 0 < x) (hz : coverLogZ x ≤ Real.log x) : coverZ x ≤ ⌊x⌋₊

The smoothness cutoff is at most the integer part of x.

theorem LongGapsBetweenPrimes.coverW_ge_two {x : ℝ} (hL : 2 ≤ Real.log x) : 2 ≤ coverW x

The small-prime cutoff is at least two when log x ≥ 2.

theorem LongGapsBetweenPrimes.eventually_smooth_count : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H : ℕ), x ≤ ↑H → ∀ S ⊆ Finset.Icc 1 H, (∀ n ∈ S, ∀ (p : ℕ), Nat.Prime p → p ∣ n → p ≤ coverZ x) → ↑S.card ≤ ↑H / Real.log x ^ 3

Eventually, at most H / (log x)^3 integers up to H are coverZ x-smooth.

theorem LongGapsBetweenPrimes.greedy_product_le {W Z : ℕ} (hW : 2 ≤ W) (hWZ : W ≤ Z) : ∏ p ∈ auxiliaryPrimes W Z, (1 - 1 / ↑p) ≤ Real.exp 6 * (1 + Real.log ↑W) / Real.log ↑Z

A logarithmic upper bound for the product of greedy survival factors.

theorem LongGapsBetweenPrimes.eventually_greedy_product_bound : ∀ᶠ (x : ℝ) in Filter.atTop, ∏ p ∈ auxiliaryPrimes (coverW x) (coverZ x), (1 - 1 / ↑p) ≤ 10 * smoothScaleConstant * Real.exp 6 * Real.log (Real.log x) ^ 2 / (Real.log x * Real.log (Real.log (Real.log x)))

The chosen cutoffs give an explicit bound for the greedy survival product.

noncomputable def LongGapsBetweenPrimes.zeroCoverPrimes (x : ℝ) : Finset ℕ

Primes assigned residue zero before the greedy covering step.

Equations

• LongGapsBetweenPrimes.zeroCoverPrimes x = (LongGapsBetweenPrimes.coverW x).primesLE ∪ ⌊x / 2⌋₊.primesLE \ (LongGapsBetweenPrimes.coverZ x).primesLE

noncomputable def LongGapsBetweenPrimes.zeroSurvivors (x : ℝ) (H : ℕ) : Finset ℕ

Integers in [1, H] surviving the initial zero-residue sieve.

Equations

• LongGapsBetweenPrimes.zeroSurvivors x H = LongGapsBetweenPrimes.survivors (Finset.Icc 1 H) (LongGapsBetweenPrimes.zeroCoverPrimes x) fun (x : ℕ) => 0

theorem LongGapsBetweenPrimes.combine_greedy_residues (S ps₀ ps₁ ps : Finset ℕ) (h₀ : ps₀ ⊆ ps) (h₁ : ps₁ ⊆ ps) (hdisj : Disjoint ps₀ ps₁) (hpos : ∀ p ∈ ps, 0 < p) : ∃ (a : ℕ → ℕ), (∀ p ∈ ps, a p < p) ∧ ↑(survivors S ps a).card ≤ ↑(survivors S ps₀ fun (x : ℕ) => 0).card * ∏ p ∈ ps₁, (1 - 1 / ↑p)

Combine a zero-residue sieve with greedy choices on a disjoint set of moduli.

theorem LongGapsBetweenPrimes.zeroSurvivors_prime_or_smooth {x : ℝ} {H n : ℕ} (hx : 0 < x) (hsmall : 2 * ↑H < x * ↑(coverW x)) (hn : n ∈ zeroSurvivors x H) : Nat.Prime n ∨ ∀ (p : ℕ), Nat.Prime p → p ∣ n → p ≤ coverZ x

A zero-sieve survivor is prime or has all prime factors at most the smoothness cutoff.

theorem LongGapsBetweenPrimes.coverW_large {x : ℝ} (hL : 2 ≤ Real.log x) : 2 * Real.log x ^ 2 < ↑(coverW x)

The small-prime cutoff exceeds 2 * (log x)^2.

theorem LongGapsBetweenPrimes.eventually_zeroSurvivors_bound : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H : ℕ), x ≤ ↑H → ↑H ≤ x * Real.log x ^ 2 → ↑(zeroSurvivors x H).card ≤ (Real.log 4 + 2) * ↑H / Real.log x

An explicit H / log x bound for the initial sieve's survivors.

noncomputable def LongGapsBetweenPrimes.coverScale (x : ℝ) : ℝ

The real scale of the interval covered by the sieve.

Equations

• LongGapsBetweenPrimes.coverScale x = x * Real.log x ^ 2 * Real.log (Real.log (Real.log x)) / Real.log (Real.log x) ^ 2

theorem LongGapsBetweenPrimes.coverLength_eq (η x : ℝ) : coverLength η x = ⌊η * coverScale x⌋₊

The covering length is the integer part of η * coverScale x.

noncomputable def LongGapsBetweenPrimes.coveringConstant : ℝ

The constant combining the initial sieve and greedy survival bounds.

Equations

• LongGapsBetweenPrimes.coveringConstant = 10 * LongGapsBetweenPrimes.smoothScaleConstant * Real.exp 6 * (Real.log 4 + 2)

theorem LongGapsBetweenPrimes.coveringConstant_pos : 0 < coveringConstant

The combined covering constant is positive.

noncomputable def LongGapsBetweenPrimes.coverEta : ℝ

A covering scale small enough to meet the short-translate density threshold.

Equations

• LongGapsBetweenPrimes.coverEta = LongGapsBetweenPrimes.sieveDelta / (2 * (1 + LongGapsBetweenPrimes.coveringConstant))

theorem LongGapsBetweenPrimes.coverEta_pos : 0 < coverEta

The chosen covering scale is positive.

theorem LongGapsBetweenPrimes.coverEta_le_one : coverEta ≤ 1

The chosen covering scale is at most one.

theorem LongGapsBetweenPrimes.coveringConstant_mul_eta_le : coveringConstant * coverEta ≤ sieveDelta

The combined covering bound fits within the sieve density threshold.

theorem LongGapsBetweenPrimes.eventually_coverLength_bounds {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) : ∀ᶠ (x : ℝ) in Filter.atTop, x < ↑(coverLength η x) ∧ ↑(coverLength η x) ≤ x * Real.log x ^ 2 ∧ η / 2 * coverScale x ≤ ↑(coverLength η x)

Eventually, the rounded covering length has the required size and retains half its scale.

theorem LongGapsBetweenPrimes.zeroCoverPrimes_subset {x : ℝ} (hx : 0 ≤ x) (hW : coverW x ≤ ⌊x⌋₊) : zeroCoverPrimes x ⊆ ⌊x⌋₊.primesLE

Every prime in the zero-residue sieve is at most x.

theorem LongGapsBetweenPrimes.zeroCoverPrimes_disjoint (x : ℝ) : Disjoint (zeroCoverPrimes x) (auxiliaryPrimes (coverW x) (coverZ x))

The zero-residue and greedy prime sets are disjoint.

theorem LongGapsBetweenPrimes.eventually_covering_residues : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (a : ℕ → ℕ), (∀ p ∈ ⌊x⌋₊.primesLE, a p < p) ∧ ↑(survivors (Finset.Icc 1 (coverLength coverEta x)) ⌊x⌋₊.primesLE a).card ≤ sieveDelta * x

For large x, residue classes leave at most sieveDelta * x integers uncovered.

theorem LongGapsBetweenPrimes.eventually_prime_gaps_in_x : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ) (q : ℕ), ConsecutivePrimes p q ∧ ↑q ≤ Real.exp (8 * x) ∧ coverEta / 2 * coverScale x ≤ ↑(q - p)

Combining the covering with Proposition 1.2 produces the long prime gaps.

theorem LongGapsBetweenPrimes.half_log_le_log_div {u c : ℝ} (hu : 0 < u) (hc : 0 < c) (h : 2 * Real.log c ≤ Real.log u) : Real.log u / 2 ≤ Real.log (u / c)

Dividing by c preserves at least half of log u when log u ≥ 2 * log c.

theorem LongGapsBetweenPrimes.eventually_coverScale_div_eight : ∀ᶠ (y : ℝ) in Filter.atTop, coverScale y / 64 ≤ coverScale (y / 8)

Rescaling by one eighth reduces coverScale by at most a factor of 64 eventually.

theorem LongGapsBetweenPrimes.gapScale_eq_coverScale_log (X : ℝ) : gapScale X = coverScale (Real.log X)

The prime-gap scale is the covering scale evaluated at log X.

theorem LongGapsBetweenPrimes.long_gap_theorem : LongGapTheorem

Theorem 1.1: the unconditional long-gap bound in the paper.

theorem LongGapsBetweenPrimes.consecutivePrimes_eq_nth {p q : ℕ} (h : ConsecutivePrimes p q) : ∃ (n : ℕ), Nat.nth Nat.Prime n = p ∧ Nat.nth Nat.Prime (n + 1) = q

Consecutive primes occur at adjacent indices in the prime enumeration.

theorem LongGapsBetweenPrimes.long_prime_gaps : ∃ (c : ℝ) (X₀ : ℝ), 0 < c ∧ ∀ (X : ℝ), X₀ ≤ X → ∃ (n : ℕ), ↑(Nat.nth Nat.Prime (n + 1)) < X ∧ c * (Real.log X * Real.log (Real.log X) ^ 2 * Real.log (Real.log (Real.log (Real.log X))) / Real.log (Real.log (Real.log X)) ^ 2) < ↑(Nat.nth Nat.Prime (n + 1)) - ↑(Nat.nth Nat.Prime n)

The long-prime-gap statement in the indexed form of Challenge.lean.