Legendre's conjecture

References:

• Landau Problems Wikipedia Page
• Legendre Conjecture Wikipedia Page
• Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

theorem LegendreConjecture.legendre_conjecture : True ↔ ∀ n ≥ 1, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Does there always exist at least one prime between consecutive perfect squares?

theorem LegendreConjecture.bounded_gap_legendre (H : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Nat.nth Nat.Prime (n + 1)) - ↑(Nat.nth Nat.Prime n) < ↑(Nat.nth Nat.Prime n) ^ (1 / 2 - c)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

If there exists a constant c > 0 such that (n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c) for all large n, then Legendre's conjecture is asymptotically true.

theorem LegendreConjecture.legendre_conjecture.ferreira_large_n : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Ferreira proved that the conjecture is true for sufficiently large n.