WeakPNT'

theorem WeakPNT' : Tendsto (fun N ↦ (∑ n ∈ Iic N, Λ n) / N) atTop (nhds 1) := by  have : (fun N ↦ (∑ n ∈ Iic N, Λ n) / N) =      (fun N ↦ (∑ n ∈ range N, Λ n)/N + Λ N / N) := by    ext N    have : N ∈ Iic N := mem_Iic.mpr (le_refl _)    rw [← Finset.sum_erase_add _ _ this, ← Nat.Iio_eq_range, Iic_erase]    exact add_div _ _ _   rw [this, ← add_zero 1]  apply Tendsto.add WeakPNT  convert squeeze_zero (f := fun N ↦ Λ N / N) (g := fun N ↦ log N / N) (t₀ := atTop) ?_ ?_ ?_  · intro N    exact div_nonneg vonMangoldt_nonneg (cast_nonneg N)  · intro N    exact div_le_div_of_nonneg_right vonMangoldt_le_log (cast_nonneg N)  have := Real.tendsto_pow_log_div_pow_atTop 1 1 Real.zero_lt_one  simp only [rpow_one] at this  exact Tendsto.comp this tendsto_natCast_atTop_atTop