internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 1 < N
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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)
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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)
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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)
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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))
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof 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
Theorem: BrunTitchmarsh.tmp
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x ^ r * x.log ^ k) =O[atTop] fun x => x ^ r * x ^ ((1 - r) / 2)
Tactic:
apply IsBigO.mul (isBigO_refl ..)
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log ^ k) =O[atTop] fun x => x ^ ((1 - r) / 2)
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log ^ k) =O[atTop] fun x => x ^ ((1 - r) / 2)
Tactic:
apply (isLittleO_log_rpow_rpow_atTop k (by linarith) ..).isBigO
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ 0 < (1 - r) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x ^ r * x ^ ((1 - r) / 2)) =ᶠ[atTop] fun N => N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
filter_upwards [Filter.eventually_gt_atTop 0]
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 0 < a → a ^ r * a ^ ((1 - r) / 2) = a * (a ^ ((1 - r) / 2))⁻¹
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 0 < a → a ^ r * a ^ ((1 - r) / 2) = a * (a ^ ((1 - r) / 2))⁻¹
Tactic:
intro N hN
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N * (N ^ ((1 - r) / 2))⁻¹
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
trans (N ^ (1 : ℝ) * (N ^ ((1-r)/2 : ℝ))⁻¹)
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N ^ 1 * (N ^ ((1 - r) / 2))⁻¹

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ 1 * (N ^ ((1 - r) / 2))⁻¹ = N * (N ^ ((1 - r) / 2))⁻¹
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N ^ 1 * (N ^ ((1 - r) / 2))⁻¹
Tactic:
rw [← Real.rpow_add hN, ← Real.rpow_neg hN.le, ← Real.rpow_add hN]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ (r + (1 - r) / 2) = N ^ (1 + -((1 - r) / 2))
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ (r + (1 - r) / 2) = N ^ (1 + -((1 - r) / 2))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ 1 * (N ^ ((1 - r) / 2))⁻¹ = N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
rw [← Nat.cast_one, Real.rpow_natCast, pow_one]
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun N => N * (N ^ ((1 - r) / 2))⁻¹) =O[atTop] fun N => N * N.log⁻¹
Tactic:
apply IsBigO.mul (isBigO_refl ..)
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => (x ^ ((1 - r) / 2))⁻¹) =O[atTop] fun x => x.log⁻¹
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => (x ^ ((1 - r) / 2))⁻¹) =O[atTop] fun x => x.log⁻¹
Tactic:
apply IsBigO.inv_rev
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log) =O[atTop] fun x => x ^ ((1 - r) / 2)

case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log) =O[atTop] fun x => x ^ ((1 - r) / 2)

case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Tactic:
apply (isLittleO_log_rpow_atTop (by linarith) ..).isBigO
Proof state after:
case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Tactic:
filter_upwards [Filter.eventually_gt_atTop 1]
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 1 < a → a.log = 0 → a ^ ((1 - r) / 2) = 0
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 1 < a → a.log = 0 → a ^ ((1 - r) / 2) = 0
Tactic:
intro N hN hcontra
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 1 < N
hcontra : N.log = 0
⊢ N ^ ((1 - r) / 2) = 0
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 1 < N
hcontra : N.log = 0
⊢ N ^ ((1 - r) / 2) = 0
Tactic:
linarith [Real.log_pos hN]
Proof state after:
no goals
Theorem: BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun N => N * N.log⁻¹) = fun N => N / N.log
Tactic:
simp_rw [div_eq_mul_inv]
Proof state after:
no goals
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x / x.log
Tactic:
calc
  _ =O[atTop] (fun x ↦ x ^ (1/2:ℝ) * (Real.log x) ^ 3) := by
    apply IsBigO.mul (isBigO_refl ..)
    apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
  _ =O[atTop] _ := by
    convert rpow_mul_rpow_log_isBigO_id_div_log 3 (?_) <;> norm_num
    rw [← Real.rpow_natCast]
    norm_cast
Proof state after:
no goals
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x ^ (1 / 2) * x.log ^ 3
Tactic:
apply IsBigO.mul (isBigO_refl ..)
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x.log ^ 3
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x.log ^ 3
Tactic:
apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
Proof state after:
no goals
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * x.log ^ 3) =O[atTop] fun x => x / x.log
Tactic:
convert rpow_mul_rpow_log_isBigO_id_div_log 3 (?_) <;> norm_num
Proof state after:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ 3 = x✝.log ^ 3
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ 3 = x✝.log ^ 3
Tactic:
rw [← Real.rpow_natCast]
Proof state after:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ ↑3 = x✝.log ^ 3
Theorem: BrunTitchmarsh.err_isBigO
Proof state before:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ ↑3 = x✝.log ^ 3
Tactic:
norm_cast
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof 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)‖
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof 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)‖
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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]
Proof 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)|
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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]
Proof 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)
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof 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)
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof 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
Theorem: BrunTitchmarsh.card_range_filter_prime_isBigO
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
rw [isPrimePow_nat_iff_bounded n] at hnprime
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
obtain ⟨p, -, k, -, hp, hk_pos, hpkn⟩ := hnprime
Proof state after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
by_cases hk : k = 1
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
right
Proof state after:
case neg.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
refine ⟨p, ?_, k, ?_, ?_⟩
Proof state after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p < √↑N

case neg.h.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ k ≤ Nat.log 2 N

case neg.h.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n = p ^ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
left
Proof state after:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime
Tactic:
rw [← hpkn, hk, pow_one]
Proof state after:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ p.Prime
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ p.Prime
Tactic:
exact hp
Proof state after:
no goals
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p < √↑N
Tactic:
rw [Real.lt_sqrt]
Proof state after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p ^ 2 < ↑N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p ^ 2 < ↑N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Tactic:
norm_cast
Proof state after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 < N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 < N
Tactic:
calc
  p^2 ≤ p^k := by
    gcongr; exact hp.one_le;omega
_ = n := hpkn
_ < N := hnN
Proof state after:
no goals
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 ≤ p ^ k
Tactic:
gcongr
Proof state after:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 1 ≤ p

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 1 ≤ p

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Tactic:
exact hp.one_le
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Tactic:
positivity
Proof state after:
no goals