feat(NumberTheory/PrimeCounting): surjective and tendsto (#17006)

Co-authored-by: Moritz Firsching <[email protected]>

Mathlib/Data/Nat/Nth.lean

@@ -303,6 +303,10 @@ theorem count_nth_of_lt_card_finite {n : ℕ} (hp : (setOf p).Finite) (hlt : n <
 theorem count_nth_of_infinite (hp : (setOf p).Infinite) (n : ℕ) : count p (nth p n) = n :=
   count_nth fun hf => absurd hf hp
 
+theorem surjective_count_of_infinite_setOf (h : {n | p n}.Infinite) :
+    Function.Surjective (Nat.count p) :=
+  fun n => ⟨nth p n, count_nth_of_infinite h n⟩
+
 theorem count_nth_succ {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card) :
     count p (nth p n + 1) = n + 1 := by rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
 

Mathlib/NumberTheory/PrimeCounting.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Bolton Bailey. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey, Ralf Stephan
 -/
-import Mathlib.Data.Nat.Totient
 import Mathlib.Data.Nat.Nth
+import Mathlib.Data.Nat.Totient
 import Mathlib.NumberTheory.SmoothNumbers
 
 /-!
@@ -56,6 +56,10 @@ def primeCounting (n : ℕ) : ℕ :=
 
 open scoped Nat.Prime
 
+@[simp]
+theorem primeCounting_sub_one (n : ℕ) : π (n - 1) = π' n := by
+  cases n <;> rfl
+
 theorem monotone_primeCounting' : Monotone primeCounting' :=
   count_monotone Prime
 
@@ -66,13 +70,38 @@ theorem monotone_primeCounting : Monotone primeCounting :=
 theorem primeCounting'_nth_eq (n : ℕ) : π' (nth Prime n) = n :=
   count_nth_of_infinite infinite_setOf_prime _
 
+@[simp]
+theorem zeroth_prime_eq_two : nth Prime 0 = 2 := nth_count prime_two
+
+/-- The `n`th prime is greater or equal to `n + 2`. -/
+theorem add_two_le_nth_prime (n : ℕ) : n + 2 ≤ nth Prime n :=
+  zeroth_prime_eq_two ▸ (nth_strictMono infinite_setOf_prime).add_le_nat n 0
+
+theorem surjective_primeCounting' : Function.Surjective π' :=
+  Nat.surjective_count_of_infinite_setOf infinite_setOf_prime
+
+theorem surjective_primeCounting : Function.Surjective π := by
+  suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
+  convert surjective_primeCounting'
+  ext
+  exact primeCounting_sub_one _
+
+open Filter
+
+theorem tendsto_primeCounting' : Tendsto π' atTop atTop := by
+  apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
+  simp [Set.range_iff_surjective.mpr surjective_primeCounting']
+
+theorem tensto_primeCounting : Tendsto π atTop atTop :=
+  (tendsto_add_atTop_iff_nat 1).mpr tendsto_primeCounting'
+
 @[simp]
 theorem prime_nth_prime (n : ℕ) : Prime (nth Prime n) :=
   nth_mem_of_infinite infinite_setOf_prime _
 
 /-- The cardinality of the finset `primesBelow n` equals the counting function
 `primeCounting'` at `n`. -/
-lemma primesBelow_card_eq_primeCounting' (n : ℕ) : n.primesBelow.card = primeCounting' n := by
+theorem primesBelow_card_eq_primeCounting' (n : ℕ) : n.primesBelow.card = primeCounting' n := by
   simp only [primesBelow, primeCounting']
   exact (count_eq_card_filter_range Prime n).symm
 
@@ -98,11 +127,4 @@ theorem primeCounting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
       rw [add_le_add_iff_left]
       exact Ico_filter_coprime_le k n h0
 
-@[simp]
-theorem zeroth_prime_eq_two : nth Prime 0 = 2 := nth_count prime_two
-
-/-- The `n`th prime is greater or equal to `n + 2`. -/
-lemma add_two_le_nth_prime (n : ℕ) : n + 2 ≤ nth Prime n :=
-  zeroth_prime_eq_two ▸ (nth_strictMono infinite_setOf_prime).add_le_nat n 0
-
 end Nat