BrunTitchmarsh.card_range_filter_isPrimePow_le

theorem card_range_filter_isPrimePow_le :    ∃ C, ∀ N, ((Finset.range N).filter IsPrimePow).card ≤ C * (N / Real.log N) := by  convert_to (fun N ↦ ((Finset.range N).filter IsPrimePow).card : ℕ → ℝ) =O[⊤]      (fun N ↦ (N / Real.log N))  · simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs]    peel with C N    by_cases hN : N = 0    · simp [hN]    rw [abs_of_nonneg]    apply Real.log_nonneg    norm_cast; omega  apply IsBigO.nat_Top_of_atTop _ _ card_isPrimePow_isBigO  have (a : ℕ) : (a : ℝ) ≠ -1 := by linarith [show 0 ≤ (a : ℝ) by positivity]  simp [this, not_isPrimePow_zero]