First Hardy–Littlewood conjecture

Reference: Wikipedia

First Hardy-Littlewood Conjecture

def IsPrimeConstellation {k : ℕ} (m : Fin k.succ → ℕ) (p : ℕ) : Prop

A prime constellation is a tuple $(p, p + m_1, ..., p + m_k)$ such that the $m_i$ are all positive even integers and every entry is a prime number.

Equations

• IsPrimeConstellation m p = (m 0 = 0 ∧ (∀ (i : Fin k.succ), i ≠ 0 → 0 < m i) ∧ ∀ (i : Fin k.succ), Nat.Prime (p + 2 * m i))

def IsAdmissiblePrimeConstellation {k : ℕ} (m : Fin k.succ → ℕ) (p : ℕ) : Prop

A prime constellation is said to be admissible if its elements do not form a complete set of residue classes with respect to any prime.

Equations

• IsAdmissiblePrimeConstellation m p = (IsPrimeConstellation m p ∧ ∀ (q : ℕ), Nat.Prime q → ¬Function.Surjective fun (i : Fin k.succ) => ↑p + 2 * ↑(m i))

def Nat.numResidues (q : ℕ) {k : ℕ} (m : Fin k.succ → ℕ) : ℕ

The number of distinct residue classes amongst a tuple $(m_0, ..., m_k)$ for a prime $q$.

Equations

• q.numResidues m = (Set.range fun (i : Fin k.succ) => ↑(m i)).ncard

def Nat.primeTupleCounting {k : ℕ} (m : Fin k.succ → ℕ) (n : ℕ) : ℕ

For a given tuple $(m_1, ..., m_k)$, this counts number of admissible prime constellations $(p, p + m_1, ..., p + m_k)$ where $p \leq n$.

Equations

• Nat.primeTupleCounting m n = Nat.count (IsAdmissiblePrimeConstellation m) n.succ

def FirstHardyLittlewoodConjectureFor {k : ℕ} (m : Fin k.succ → ℕ) : Prop

Equations

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

theorem first_hardy_littlewood_conjecture {k : ℕ} (m : Fin k.succ → ℕ) : FirstHardyLittlewoodConjectureFor m

Let $P = (m_1, ..., m_k)$ be a tuple of positive even integers. Let $\pi_P(n)$ denote the number of primes $p\leq n$ such that $(p, p + m_1, ..., p + m_k)$ forms an admissible prime constellation. Let $w(q; m_1, ..., m_k)$ denote the number of distinct residues of $0, m_1, ..., m_k$ modulo $q$, and let $$ C_P = 2 ^ k\prod_{\substack{q\ \text{prime} \\ q\geq 3}} \frac{1 - \frac{w(q; m_1, ..., m_k)}{q}}{\left(1 - \frac{1}{q}\right)^{k+1}}. $$ Then $$ \pi_P(n)\tilde C_P\int_2^n\frac{dt}{\log^{k+1}t}. $$

Second Hardy-Littlewood Conjecture

def SecondHardyLittlewoodConjectureFor (x y : ℕ) : Prop

Equations

• SecondHardyLittlewoodConjectureFor x y = ((x + y).primeCounting ≤ x.primeCounting + y.primeCounting)

theorem second_hardy_littlewood_conjecture {x y : ℕ} (hx : 2 ≤ x) (hy : 2 ≤ y) : SecondHardyLittlewoodConjectureFor x y

For integers $x, y \geq 2$, $$ \pi(x + y) \leq \pi(x) + \pi(y), $$ where $\pi(z)$ denotes the prime-counting function, giving the number of primes up to and including $z$.

theorem not_first_and_secondHardyLittlewoodConjecture : (∀ {k : ℕ} (m : Fin k.succ → ℕ), FirstHardyLittlewoodConjectureFor m) → ¬∀ {x y : ℕ}, 2 ≤ x → 2 ≤ y → SecondHardyLittlewoodConjectureFor x y

Richards [Ri74] showed that only one of the two Hardy-Littlewood conjectures can be true.

[Ri74] Richards, Ian (1974). On the Incompatibility of Two Conjectures Concerning Primes. Bull. Amer. Math. Soc. 80: 419–438.