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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun 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 => ↑N / (↑N).log
Tactic:
apply IsBigO.trans ?_ pow_half_mul_one_add_log_div_isBigO.natCast
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun 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 => ↑n ^ (1 / 2) * (1 + (↑n).log / Real.log 2)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun 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 => ↑n ^ (1 / 2) * (1 + (↑n).log / Real.log 2)
Tactic:
apply isBigO_of_le
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑x ^ (1 / 2) * (1 + (↑x).log / Real.log 2)‖

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

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

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

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑N ^ 2⁻¹ * (1 + (↑N).log / Real.log 2)

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Tactic:
convert pows_small_primes_le N using 3
State after:
case h.e'_4.h.e'_5.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 2⁻¹ = 1 / 2

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2

State before:
case h.e'_4.h.e'_5.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 2⁻¹ = 1 / 2

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Tactic:
norm_num
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Tactic:
by_cases hN : N = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ 0 ≤ 1 + (↑N).log / Real.log 2

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ 1 + (↑N).log / Real.log 2

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Tactic:
rw [Real.log_div_log]
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ 1 + Real.logb 2 ↑N

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ 1 + Real.logb 2 ↑N
Tactic:
linarith [Real.logb_nonneg (show 1 < (2:ℝ) by norm_num) (show (1 : ℝ) ≤ N by norm_num; omega)]
State after:
no goals

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

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Tactic:
simp [hN]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N
Tactic:
norm_num
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N

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