Bonse's inequality

TheoremInfinitely many primes#✓fully proved

The set of prime natural numbers is infinite.

Here a natural number \(p\) is prime in the sense of prime elements of a commutative monoid with zero: \(p\) is neither \(0\) nor a unit, and \(p \mid ab\) implies \(p \mid a\) or \(p \mid b\). For natural numbers this agrees with the usual notion of a prime number.

theorem bonse_primes_infinite : (Set.ofPred fun p : ℕ => Prime p).Infinite
Used by 2
Used byThe enumeration of the primes takes prime values · The enumeration of the primes is strictly increasing

TheoremThe enumeration of the primes is strictly increasing#✓fully proved

For \(k \ge 1\) let \(p_k\) be the \(k\)-th smallest prime number. If \(i < j\), then \(p_i < p_j\).

theorem bonse_nth_strictMono : StrictMono (Nat.nth Prime)
Uses 1 · Used by 2
Proof usesInfinitely many primes
Used byBonse's inequality · Bertrand's postulate for consecutive primes

TheoremThe enumeration of the primes takes prime values#✓fully proved

For every \(k \ge 1\), the \(k\)-th smallest prime number exists and is prime.

theorem bonse_nth_prime (k : ℕ) : Prime (Nat.nth Prime k)
Uses 1 · Used by 1
Proof usesInfinitely many primes
Used byBertrand's postulate for consecutive primes

TheoremThe sixth prime is thirteen#✓fully proved

The sixth prime number, counting \(2\) as the first, is \(13\).

theorem bonse_nth_five : Nat.nth Prime 5 = 13
Used by 1
Used byBonse's inequality

TheoremBertrand's postulate for consecutive primes#✓fully proved

Let \(p_1 < p_2 < p_3 < \cdots\) be the prime numbers in increasing order. For every \(k \ge 1\), \(p_{k+1} < 2 p_k\).

theorem bonse_nth_succ_lt (k : ℕ) :
    Nat.nth Prime (k + 1) < 2 * Nat.nth Prime k
Uses 2 · Used by 1
Proof usesThe enumeration of the primes takes prime values · The enumeration of the primes is strictly increasing
Used byBonse's inequality

TheoremBonse's inequality#✓fully proved

Let \(p_1 = 2, p_2 = 3, p_3 = 5, \dots\) be the prime numbers in increasing order. For every natural number \(k > 4\), the square of the \((k+1)\)-st prime is smaller than the product of the first \(k\) primes: \(p_{k+1}^2 < p_1 p_2 \cdots p_k\).

theorem bonse_inequality
    (k : ℕ) (hk : 4 < k) :
    (Nat.nth Prime k) ^ 2 < ∏ i ∈ Finset.range k, Nat.nth Prime i
Sources
Uses 3
Proof usesThe sixth prime is thirteen · The enumeration of the primes is strictly increasing · Bertrand's postulate for consecutive primes

DefinitionThe \(m\)-th prime, counted from one#✓fully proved

For \(m \ge 1\), \(p_m\) is the \(m\)-th prime, so that \(p_1 = 2\), \(p_2 = 3\), \(p_3 = 5\); at \(m = 0\) the value is also \(2\).

noncomputable def primeNth (m : ℕ) : ℕ := Nat.nth Nat.Prime (m - 1)
Used by 1
Used byBonse sequence of prime indices

DefinitionBonse sequence of prime indices#✓fully proved

For \(m \ge 1\) let \(p_m\) be the \(m\)-th prime, so that \(p_1 = 2\), and set \(p_0 = 2\). A sequence \(a_0, a_1, a_2, \ldots\) of natural numbers is a Bonse sequence if \(p_{a_n}^2 < p_{a_0} p_{a_1} \cdots p_{a_{n-1}}\) for all sufficiently large \(n\).

In the paper's 1-based indexing the condition reads \(p_{a_1} \cdots p_{a_n} > p_{a_{n+1}}^2\) for all sufficiently large \(n\).

def IsBonseSeq (a : ℕ → ℕ) : Prop :=
  ∀ᶠ n in atTop, (primeNth (a n) : ℝ) ^ 2 <
    ∏ k ∈ Finset.range n, (primeNth (a k) : ℝ)
Uses 1 · Used by 2
Statement usesThe \(m\)-th prime, counted from one
Used byA sufficient condition for a Bonse sequence · A sufficient condition for a non-Bonse sequence

TheoremA sufficient condition for a Bonse sequence#●ready to prove

Let \(a_0 < a_1 < a_2 < \cdots\) be a strictly increasing sequence of positive integers and write \(A_n = a_0 a_1 \cdots a_{n-1}\) for the product of its first \(n\) terms. If there is a real number \(c > 2\) such that \(\log A_n / \log a_n > c\) for all sufficiently large \(n\), then \(a\) is a Bonse sequence.

The hypothesis is equivalent to \(\liminf_n \log A_n / \log a_n > 2\), an infinite limit inferior included. In the paper's 1-based indexing it reads \(\liminf \log A_n / \log a_{n+1} > 2\) with \(A_n = a_1 \cdots a_n\).

theorem_wanted isBonseSeq_of_liminf_gt (a : ℕ → ℕ)
    (hmono : StrictMono a) (hpos : ∀ n, 1 ≤ a n)
    (hlim : ∃ c : ℝ, 2 < c ∧ ∀ᶠ n in atTop,
      c < Real.log (∏ k ∈ Finset.range n, (a k : ℝ)) /
        Real.log (a n)) :
    IsBonseSeq a
Sources
  • Diego Marques, "Bonse's Inequality along Subsequences of Primes", Theorem 1.
Uses 1
Statement usesBonse sequence of prime indices

TheoremA sufficient condition for a non-Bonse sequence#●ready to prove

Let \(a_0 < a_1 < a_2 < \cdots\) be a strictly increasing sequence of positive integers and write \(A_n = a_0 a_1 \cdots a_{n-1}\) for the product of its first \(n\) terms. Suppose that \((n + 1) \log \log a_n / \log a_{n+1} \to 0\) as \(n \to \infty\), and that there is a real number \(c < 2\) such that \(\log A_n / \log a_n < c\) for infinitely many \(n\). Then \(a\) is not a Bonse sequence.

The second hypothesis is equivalent to \(\liminf_n \log A_n / \log a_n < 2\). In the paper's 1-based indexing the hypotheses read \(n \log \log a_n / \log a_{n+1} \to 0\) and \(\liminf \log A_n / \log a_{n+1} < 2\) with \(A_n = a_1 \cdots a_n\).

theorem_wanted not_isBonseSeq_of_liminf_lt (a : ℕ → ℕ)
    (hmono : StrictMono a) (hpos : ∀ n, 1 ≤ a n)
    (hreg : Tendsto (fun n : ℕ =>
      ((n : ℝ) + 1) * Real.log (Real.log (a n)) /
        Real.log (a (n + 1))) atTop (𝓝 0))
    (hlim : ∃ c : ℝ, c < 2 ∧ ∃ᶠ n in atTop,
      Real.log (∏ k ∈ Finset.range n, (a k : ℝ)) /
        Real.log (a n) < c) :
    ¬ IsBonseSeq a
Sources
  • Diego Marques, "Bonse's Inequality along Subsequences of Primes", Theorem 2.
Uses 1
Statement usesBonse sequence of prime indices
8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.