Source indexedlemma · leanprover/lean4:v4.32.0

pi_nth_prime_asymp

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:922 to 932

Mathematical statement

Exact Lean statement

lemma pi_nth_prime_asymp :
    (fun n ↦ (nth_prime n) / (log (nth_prime n))) ~[atTop] (fun (n : ℕ) ↦ (n : ℝ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pi_nth_prime_asymp :    (fun n ↦ (nth_prime n) / (log (nth_prime n))) ~[atTop] (fun (n : ℕ) ↦ (n : ℝ)) := by  trans (fun (n : ℕ) ↦ ( n + 1 : ℝ))  · have : Tendsto (fun n ↦ ((nth_prime n) : ℝ)) atTop atTop := by      apply tendsto_natCast_atTop_iff.mpr tendsto_nth_prime_atTop    convert! pi_alt'.comp_tendsto this |>.symm    simp only [Function.comp_apply, floor_natCast]    rw [pi_nth_prime]    norm_cast  · apply IsEquivalent.add_isLittleO (by rfl)    exact isLittleO_const_id_atTop (1 : ℝ) |>.natCast_atTop