Lemma 5.1 — at least $\eta x/(2\log x)$ primes in $((1-2\eta)x,(1-\eta)x]$

Open

IntMul.HvdH.lemma_5_1

by avi · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprimes

Let $\eta$ be a real number with $0<\eta<\tfrac14$ , and let $x$ be a real number with $x\ge e^{2/\eta}$ . Then the interval $\big((1-2\eta)x,(1-\eta)x\big]$ contains many primes:

\#\{q\text{ prime}:(1-2\eta)x<q\le(1-\eta)x\}\ \ge\ \frac{\eta x}{2\log x}.

Here $\log$ is the natural logarithm. In the paper this lemma supplies $d$ distinct primes $s_1,\dots,s_d$ slightly below the power-of-two lengths $t_1,\dots,t_d$ , so that every ratio $t_i/s_i$ stays away from $1$ while the product $t_1\cdots t_d/(s_1\cdots s_d)$ stays bounded.

Preamble

import Mathlib

Formal statement

namespace IntMul.HvdH

theorem lemma_5_1 (η : ℝ) (hη₀ : 0 < η) (hη₁ : η < 1 / 4) (x : ℝ) (hx : Real.exp (2 / η) ≤ x) :
    η * x / (2 * Real.log x) ≤
      ({q : ℕ | q.Prime ∧ (1 - 2 * η) * x < q ∧ (q : ℝ) ≤ (1 - η) * x}.ncard : ℝ) := by sorry

end IntMul.HvdH

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2) (2021) 563-617, https://doi.org/10.4007/annals.2021.193.2.4 (preprint https://hal.science/hal-02070778v2), §5.2, Lemma 5.1, p. 37

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Statement. Let $\eta$ be a real number with

0 < \eta < \tfrac14 \quad(\text{both strict}),

and let $x$ be a real number with

x \ge e^{2/\eta} \quad(\text{non-strict}).

Then the number of primes in the half-open interval $\big((1-2\eta)x,\ (1-\eta)x\big]$ is at least $\dfrac{\eta x}{2\log x}$ :

\frac{\eta\, x}{2\log x} \;\le\; \#\big\{\, q \in \mathbb{N} \;:\; q \text{ is prime},\ (1-2\eta)x < q \le (1-\eta)x \,\big\}.

Binders and hypotheses. There are exactly two universally quantified variables, the real numbers $\eta$ and $x$ , and three hypotheses: $0<\eta$ (strict), $\eta < 1/4$ (strict), and $e^{2/\eta} \le x$ (non-strict). No other assumptions are made; in particular $x$ need not be an integer.

Meaning of the symbols.

$\log$ is the natural logarithm (base $e$ ), and $e^{2/\eta}$ is the real exponential.
$q$ ranges over natural numbers that are prime (so $q \ge 2$ ); the comparisons with $(1-2\eta)x$ and $(1-\eta)x$ are made after viewing $q$ as a real number. The lower endpoint is excluded (strict $<$ ) and the upper endpoint is included ( $\le$ ).
$\#$ denotes the cardinality of the set, returned as a natural number and then regarded as a real number for the comparison. (The counting function used assigns the value $0$ to an infinite set; here the set is always finite, since every element satisfies $q \le (1-\eta)x$ , so the count is the genuine number of such primes.)
The inequality is a non-strict $\le$ between two real numbers.

Edge cases and remarks on the hypothesis range. The hypotheses are jointly satisfiable (e.g. $\eta = 1/8$ , $x = e^{16}$ ). Since $0<\eta<1/4$ , we have $2/\eta > 8$ , so $x \ge e^{2/\eta} > e^8 \approx 2981$ ; hence $\log x \ge 2/\eta > 8 > 0$ , the denominator $2\log x$ is strictly positive, and no division-by-zero or junk value arises. Also $1-2\eta \in (1/2, 1)$ and $1-\eta \in (3/4,1)$ , so the interval $\big((1-2\eta)x, (1-\eta)x\big]$ is a non-empty interval of positive reals of length $\eta x$ , lying strictly below $x$ . The left-hand side $\eta x/(2\log x)$ is a positive real number, not rounded to an integer, so the statement in particular asserts the interval contains at least one prime.

Human review

Endorsed by wurtle · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by avi · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 5.1 — at least ηx/(2log⁡x)\eta x/(2\log x)ηx/(2logx) primes in ((1−2η)x,(1−η)x]((1-2\eta)x,(1-\eta)x]((1−2η)x,(1−η)x]

Lemma 5.1 — at least $\eta x/(2\log x)$ primes in $((1-2\eta)x,(1-\eta)x]$