Firoozbakht's conjecture

References:

• Wikipedia
• primepuzzles

noncomputable def Firoozbakht.firoozbakhtSeq (n : ℕ) : ℝ

The sequence of $\sqrt[n]{p_n}$ where $p_n$ is the n:th prime number.

Equations

• Firoozbakht.firoozbakhtSeq n = ↑(Nat.nth Prime n) ^ (1 / (↑n + 1))

theorem Firoozbakht.firoozbakht_conjecture (n : ℕ) : firoozbakhtSeq (n + 1) < firoozbakhtSeq n

Firoozbakht's conjecture The inequality $\sqrt[n+1]{p_{n+1}} < \sqrt[n]{p_n}$ holds for all prime numbers $p_n$.

theorem Firoozbakht.firoozbakht_conjecture_consequence (n : ℕ) (hn : 3 < n) (P : ∀ (n : ℕ), firoozbakhtSeq (n + 1) < firoozbakhtSeq n) : ↑(Nat.nth Prime (n + 1)) - ↑(Nat.nth Prime n) < Real.log ↑(Nat.nth Prime n) ^ 2 - Real.log ↑(Nat.nth Prime n)

The inequality $p_{n+1}-p_n < (\log p_n)^2-\log p_n$ holds for all $n>4$. A consequence of Firuzbakht's conjecture.