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

State before:
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:
trans ↑((Finset.range (N+1)).filter Nat.Prime).card
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card

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

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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
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
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

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

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
by_cases hN : N = 1
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
have h : primesBetween 1 (1 + N) ≤
    2 * (N / Real.log (N^(1/2:ℝ))) + 6 * (N ^ (1 / 2 : ℝ) * (1 + Real.log (N ^ (1 / 2 : ℝ))) ^ 3) := by
  convert (primesBetween_le 1 N (N ^ (1/2 : ℝ)) (by norm_num) (by norm_cast; omega)
    (Real.one_lt_rpow (by norm_cast; omega) (by norm_num))) using 1
  ring
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
calc
  _ ≤ (primesBetween 1 (1+N):ℝ) := by
    norm_cast; apply primesBetween_mono_right; norm_cast; omega
  _ ≤ _ := by
    rw [Real.log_rpow (by norm_num; omega)] at h
    convert h using 2
    ring
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card
Tactic:
norm_cast
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card
Tactic:
apply Finset.card_le_card
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))
Tactic:
intro n
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))
Tactic:
simp only [Finset.mem_filter, Finset.mem_range, and_imp]
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → n.Prime → n < N + 1 ∧ n.Prime

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → n.Prime → n < N + 1 ∧ n.Prime
Tactic:
refine fun hnN hp ↦ ⟨by omega, hp⟩
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hp : n.Prime
⊢ n < N + 1
Tactic:
omega
State after:
no goals

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

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
simp (config := {decide:=true}) [hN, primesBetween]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
Tactic:
convert (primesBetween_le 1 N (N ^ (1/2 : ℝ)) (by norm_num) (by norm_cast; omega)
  (Real.one_lt_rpow (by norm_cast; omega) (by norm_num))) using 1
State after:
case h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3) =
    2 * ↑N / (↑N ^ (1 / 2)).log + 6 * ↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3

State before:
case h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3) =
    2 * ↑N / (↑N ^ (1 / 2)).log + 6 * ↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3
Tactic:
ring
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 0 < 1
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
hN : ¬N = 1
⊢ 0 < ↑N
Tactic:
norm_cast
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 0 < N

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

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

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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 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
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 ↑N) ≤ ↑(primesBetween 1 (1 + ↑N))
Tactic:
norm_cast
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ primesBetween 1 ↑N ≤ primesBetween 1 ↑(1 + N)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ primesBetween 1 ↑N ≤ primesBetween 1 ↑(1 + N)
Tactic:
apply primesBetween_mono_right
State after:
case hbc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑N ≤ ↑(1 + N)

State before:
case hbc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑N ≤ ↑(1 + N)
Tactic:
norm_cast
State after:
case hbc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ N ≤ 1 + N

State before:
case hbc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ N ≤ 1 + N
Tactic:
omega
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 (1 + ↑N)) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
rw [Real.log_rpow (by norm_num; omega)] at h
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (1 / 2 * (↑N).log)) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
⊢ ↑(primesBetween 1 (1 + ↑N)) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (1 / 2 * (↑N).log)) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
⊢ ↑(primesBetween 1 (1 + ↑N)) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
convert h using 2
State after:
case h.e'_4.h.e'_5
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (1 / 2 * (↑N).log)) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
⊢ 4 * (↑N / (↑N).log) = 2 * (↑N / (1 / 2 * (↑N).log))

State before:
case h.e'_4.h.e'_5
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (1 / 2 * (↑N).log)) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
⊢ 4 * (↑N / (↑N).log) = 2 * (↑N / (1 / 2 * (↑N).log))
Tactic:
ring
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ 0 < ↑N
Tactic:
norm_num
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ 0 < N

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ 0 < N
Tactic:
omega
State after:
no goals