Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
Tactic:
convert_to (fun N ↦ ((Finset.range N).filter IsPrimePow).card : ℕ → ℝ) =O[⊤] (fun N ↦ (N / Real.log N))
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
Tactic:
apply IsBigO.nat_Top_of_atTop _ _ card_isPrimePow_isBigO
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (n : ℕ), ↑n / (↑n).log = 0 → ↑(Finset.filter IsPrimePow (Finset.range n)).card = 0

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (n : ℕ), ↑n / (↑n).log = 0 → ↑(Finset.filter IsPrimePow (Finset.range n)).card = 0
Tactic:
simp only [div_eq_zero_iff, Nat.cast_eq_zero, Real.log_eq_zero, Nat.cast_eq_one, or_self_left,
  Finset.card_eq_zero, forall_eq_or_imp, Finset.range_zero, Finset.filter_empty, Finset.range_one,
  true_and]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter IsPrimePow {0} = ∅ ∧ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter IsPrimePow {0} = ∅ ∧ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
refine ⟨rfl, ?_⟩
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
intro a ha
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ Finset.filter IsPrimePow (Finset.range a) = ∅

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
exfalso
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ False

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ False
Tactic:
linarith [show 0 ≤ (a : ℝ) by positivity]
State after:
no goals

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
Tactic:
simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs]
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    ∃ C, ∀ (x : ℕ), ↑(Finset.filter IsPrimePow (Finset.range x)).card ≤ C * (↑x / |(↑x).log|)

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    ∃ C, ∀ (x : ℕ), ↑(Finset.filter IsPrimePow (Finset.range x)).card ≤ C * (↑x / |(↑x).log|)
Tactic:
peel with C N
State after:
case a.h.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)

State before:
case a.h.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
by_cases hN : N = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
rw [abs_of_nonneg]
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ (↑N).log

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ (↑N).log
Tactic:
apply Real.log_nonneg
State after:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N

State before:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N
Tactic:
norm_cast
State after:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N

State before:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N
Tactic:
omega
State after:
no goals

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
simp [hN]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ 0 ≤ ↑a
Tactic:
positivity
State after:
no goals