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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[atTop] fun N =>
    ↑(Finset.filter Nat.Prime (Finset.range N) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
apply isBigO_of_le
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter IsPrimePow (Finset.range x)).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter IsPrimePow (Finset.range x)).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Tactic:
simp only [RCLike.norm_natCast, Nat.cast_le]
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    (Finset.filter IsPrimePow (Finset.range x)).card ≤
      (Finset.filter Nat.Prime (Finset.range x) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    (Finset.filter IsPrimePow (Finset.range x)).card ≤
      (Finset.filter Nat.Prime (Finset.range x) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card
Tactic:
intro N
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter IsPrimePow (Finset.range N)).card ≤
    (Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter IsPrimePow (Finset.range N)).card ≤
    (Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
apply Finset.card_le_card
State after:
case hfg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter IsPrimePow (Finset.range N) ⊆
    Finset.filter Nat.Prime (Finset.range N) ∪
      Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))

State before:
case hfg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter IsPrimePow (Finset.range N) ⊆
    Finset.filter Nat.Prime (Finset.range N) ∪
      Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))
Tactic:
apply range_filter_isPrimePow_subset_union
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N =>
      ↑(Finset.filter Nat.Prime (Finset.range N) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun N =>
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
apply isBigO_of_le
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Tactic:
simp only [RCLike.norm_natCast, Real.norm_eq_abs]
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ↑(Finset.filter Nat.Prime (Finset.range x) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card ≤
      |↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card|

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ↑(Finset.filter Nat.Prime (Finset.range x) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card ≤
      |↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card|
Tactic:
intro N
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    |↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card|

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    |↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card|
Tactic:
rw [abs_of_nonneg (by positivity)]
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
norm_cast
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.filter Nat.Prime (Finset.range N)).card +
      (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.filter Nat.Prime (Finset.range N)).card +
      (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
apply Finset.card_union_le
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
positivity
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N =>
      ↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
Tactic:
apply IsBigO.add
State after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.filter Nat.Prime (Finset.range x)).card) =O[atTop] fun N => ↑N / (↑N).log

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log

State before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
Tactic:
apply card_pows_aux
State after:
no goals

State before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.filter Nat.Prime (Finset.range x)).card) =O[atTop] fun N => ↑N / (↑N).log
Tactic:
exact card_range_filter_prime_isBigO
State after:
no goals