Ramanujan primes

DefinitionLabos prime#✓fully proved

Write \(\pi(x)\) for the number of primes \(p \le x\). For natural numbers \(n\) and \(L\), \(L\) is the \(n\)-th Labos prime when \(n \ge 1\), \(L \ge 1\), \(\pi(L) - \pi(\lfloor L/2 \rfloor) = n\), and no integer \(m\) with \(1 \le m < L\) satisfies \(\pi(m) - \pi(\lfloor m/2 \rfloor) = n\); that is, \(L\) is the least positive integer with \(\pi(L) - \pi(\lfloor L/2 \rfloor) = n\).

def IsLabosPrime (n L : ℕ) : Prop :=
  1 ≤ n ∧ 0 < L ∧ Nat.primeCounting L - Nat.primeCounting (L / 2) = n ∧
    ∀ m, 0 < m → m < L → Nat.primeCounting m - Nat.primeCounting (m / 2) ≠ n

DefinitionPrimes satisfying the Ramanujan counting condition#✓fully proved

Let \(\pi\) be the prime-counting function. For natural numbers \(R\) and \(n\), \(R\) satisfies the Ramanujan counting condition for \(n\) when \(R\) is prime and \(\pi(R) - \pi(R/2) = n\).

Here \(\pi(x)\) counts the primes \(p \le x\), so \(\pi(R/2) = \pi(\lfloor R/2 \rfloor)\).

public def IsRamanujanPrime (R n : ℕ) : Prop :=
  Nat.Prime R ∧ (Nat.primeCounting R - Nat.primeCounting (R / 2) = n)

Used by 1

Used byThe \(n\)-th Ramanujan prime

DefinitionThe \(n\)-th Ramanujan prime#✓fully proved

Let \(\pi\) be the prime-counting function. For natural numbers \(R\) and \(n\), \(R\) is the \(n\)-th Ramanujan prime when \(n \ge 1\), \(R\) is a prime with \(\pi(R) - \pi(R/2) = n\), and every prime \(p\) with \(\pi(p) - \pi(p/2) = n\) satisfies \(p \le R\). That is, \(R\) is the largest prime satisfying the Ramanujan counting condition for \(n\).

Here \(\pi(x)\) counts the primes \(p \le x\), so \(\pi(R/2) = \pi(\lfloor R/2 \rfloor)\).

public def IsNthRamanujanPrime (R n : ℕ) : Prop :=
  1 ≤ n ∧ IsRamanujanPrime R n ∧ ∀ p : ℕ, IsRamanujanPrime p n → p ≤ R

Uses 1 · Used by 1

Statement usesPrimes satisfying the Ramanujan counting condition

Used byLaishram's upper bound for Ramanujan primes

DefinitionCounting members of a set up to a real bound#✓fully proved

For a set \(P\) of natural numbers and a real number \(x\), \(\pi_P(x)\) is the number of members of \(P\) that are at most \(x\).

In the intended application \(P\) is an infinite set of primes.

noncomputable def primeCountingWithin (P : Set ℕ) (x : ℝ) : ℕ :=
  Set.ncard {p : ℕ | p ∈ P ∧ (p : ℝ) ≤ x}

Used by 1

Used byGeneralized Ramanujan numbers

DefinitionGeneralized Ramanujan numbers#✓fully proved

Let \(P\) be a set of natural numbers, \(v\) a real number and \(m\), \(R\) natural numbers, and write \(\pi_P(x)\) for the number of members of \(P\) that are at most \(x\). Then \(R\) is the \((v, P)\)-Ramanujan number of index \(m\) when \(P\) is an infinite set of primes, \(v > 1\), and \(R\) is the least natural number such that \(\pi_P(x) - \pi_P(x/v) \ge m\) for every real \(x \ge R\), that is, every interval \((x/v, x]\) with \(x \ge R\) contains at least \(m\) members of \(P\).

def IsVPRamanujanNumber (P : Set ℕ) (v : ℝ) (m R : ℕ) : Prop :=
  P.Infinite ∧
    P ⊆ {p : ℕ | p.Prime} ∧
    1 < v ∧
    Minimal {R' : ℕ |
      ∀ x : ℝ, (R' : ℝ) ≤ x →
        (m : ℤ) ≤ (primeCountingWithin P x : ℤ) - (primeCountingWithin P (x / v) : ℤ)} R

Uses 1

Statement usesCounting members of a set up to a real bound

TheoremLaishram's upper bound for Ramanujan primes#●ready to prove

Let \(p_k\) denote the \(k\)-th prime, so that \(p_1 = 2\). For all natural numbers \(n\) and \(R\), if \(R\) is the \(n\)-th Ramanujan prime (which entails \(n \ge 1\)), then \(R < p_{3n}\).

theorem_wanted laishram_ramanujan_prime_bound (n R : ℕ)
    (hR : IsNthRamanujanPrime R n) :
    R < Nat.nth Nat.Prime (3 * n - 1)

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL14/Noe/noe12.tex, theorem lines 152-160, definition lines 105-117.

Uses 1

Statement usesThe \(n\)-th Ramanujan prime

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.