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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter Nat.Prime (Finset.range N)).card) =O[atTop] fun N =>
    4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
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)).card‖ ≤
      ‖4 * (↑x / (↑x).log) + 6 * (↑x ^ (1 / 2) * (1 + 1 / 2 * (↑x).log) ^ 3)‖

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter Nat.Prime (Finset.range x)).card‖ ≤
      ‖4 * (↑x / (↑x).log) + 6 * (↑x ^ (1 / 2) * (1 + 1 / 2 * (↑x).log) ^ 3)‖
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)).card‖ ≤
    ‖4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)‖

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ‖↑(Finset.filter Nat.Prime (Finset.range N)).card‖ ≤
    ‖4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)‖
Tactic:
simp only [RCLike.norm_natCast, one_div, Real.norm_eq_abs]
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ |4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)|

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ |4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)|
Tactic:
rw [abs_of_nonneg]
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)
Tactic:
convert tmp N using 4 <;> norm_num
State after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)

State before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)
Tactic:
positivity
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)) =O[atTop] fun N => ↑N / (↑N).log
Tactic:
apply ((isBigO_refl ..).const_mul_left ..).add
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 6 * (↑x ^ (1 / 2) * (1 + 1 / 2 * (↑x).log) ^ 3)) =O[atTop] fun N => ↑N / (↑N).log

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 6 * (↑x ^ (1 / 2) * (1 + 1 / 2 * (↑x).log) ^ 3)) =O[atTop] fun N => ↑N / (↑N).log
Tactic:
apply err_isBigO.natCast.const_mul_left
State after:
no goals