Prime-indexed primes

TheoremRatio of consecutive zero-based prime-indexed primes tends to one#✓fully proved

Let \(p_0 = 2\), \(p_1 = 3\), \(p_2 = 5\), \(\dots\) be the primes in increasing order, indexed from zero, and let \(q_n = p_{p_n}\). Then \(q_n / q_{n+1} \to 1\) as \(n \to \infty\).

public theorem primePrimes_ratio_tendsto_one' :
    Filter.Tendsto (fun n : ℕ =>
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime n) : ℕ) : ℝ) /
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime (n + 1)) : ℕ) : ℝ))
      Filter.atTop (nhds 1)

Uses 1 · Used by 1

Proof usesPrime number theorem

Used byBroughan–Barnett ratio limit, zero-based form

TheoremRatio of consecutive prime-indexed primes tends to one#✓fully proved

Let \(p_1 = 2\), \(p_2 = 3\), \(p_3 = 5\), \(\dots\) be the primes in increasing order and let \(q_n = p_{p_n}\). Then \(q_n / q_{n+1} \to 1\) as \(n \to \infty\).

This is part (c) of the Broughan–Barnett corollary, in the source's one-based indexing.

public theorem primePrimes_oneBased_ratio_tendsto_one :
    Filter.Tendsto (fun n : ℕ =>
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime n - 1) : ℕ) : ℝ) /
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime (n + 1) - 1) : ℕ) : ℝ))
      Filter.atTop (nhds 1)

Uses 1

Proof usesPrime number theorem

TheoremBroughan–Barnett ratio limit, zero-based form#✓fully proved

Assume that there are infinitely many primes (which always holds). Let \(p_0 = 2\), \(p_1 = 3\), \(p_2 = 5\), \(\dots\) be the primes in increasing order, indexed from zero, and let \(q_n = p_{p_n}\). Then \(q_n / q_{n+1} \to 1\) as \(n \to \infty\).

In the source's one-based indexing \(p'_1 = 2\), \(p'_2 = 3\), \(\dots\), this \(q_n\) equals \(p'_{p'_{n+1} + 1}\) rather than the source's prime-indexed prime \(p'_{p'_{n+1}}\); the source states the same limit for its sequence.

public theorem primePrimes_ratio_tendsto_one
    [Infinite { n : ℕ // n.Prime }] :
    Filter.Tendsto (fun n : ℕ =>
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime n) : ℕ) : ℝ) /
      ((Nat.nth Nat.Prime (Nat.nth Nat.Prime (n + 1)) : ℕ) : ℝ))
      Filter.atTop (nhds 1)

Sources

• Kevin A. Broughan and A. Ross Barnett, "On the Subsequence of Primes Having Prime Subscripts," Journal of Integer Sequences 12 (2009), Article 09.2.3, Corollary to the Theorem, part (c), lines 193–199, https://cs.uwaterloo.ca/journals/JIS/VOL12/Broughan/broughan16.tex

Uses 1

Proof usesRatio of consecutive zero-based prime-indexed primes tends to one

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.