internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
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
Tactic:
calc
  _ ≤ Nat.log p n := by
    apply Nat.le_log_of_pow_le hp.one_lt hpkn.le
  _ ≤ Nat.log 2 n := by
    apply Nat.log_anti_left (by norm_num) hp.two_le
  _ ≤ Nat.log 2 N := by
    apply Nat.log_mono_right hnN.le
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
⊢ k ≤ p.log n
Tactic:
apply Nat.le_log_of_pow_le hp.one_lt hpkn.le
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.log n ≤ Nat.log 2 n
Tactic:
apply Nat.log_anti_left (by norm_num) hp.two_le
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
⊢ 1 < 2
Tactic:
norm_num
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
⊢ Nat.log 2 n ≤ Nat.log 2 N
Tactic:
apply Nat.log_mono_right hnN.le
Proof state after:
no goals
Theorem: BrunTitchmarsh.prime_or_pow
Proof state before:
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
Tactic:
exact hpkn.symm
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
apply le_antisymm
Proof state after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n ≤ ⌊(↑b).logb ↑n⌋₊

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ⌊(↑b).logb ↑n⌋₊ ≤ b.log n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
apply Real.logb_nonneg
Proof state after:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 < ↑b

case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 < ↑b
Tactic:
norm_cast
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ ↑n
Tactic:
norm_cast
Proof state after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_iff_ne_zero.mpr hn
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n ≤ ⌊(↑b).logb ↑n⌋₊
Tactic:
rw [Nat.le_floor_iff, Real.le_logb_iff_rpow_le]
Proof state after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑(b.log n) ≤ ↑n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑(b.log n) ≤ ↑n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
norm_cast
Proof state after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ b.log n ≤ n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ b.log n ≤ n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
apply Nat.pow_log_le_self
Proof state after:
case neg.a.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ n ≠ 0

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ n ≠ 0
Tactic:
exact hn
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b
Tactic:
norm_cast
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n
Tactic:
norm_cast
Proof state after:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < n
Tactic:
exact Nat.zero_lt_of_ne_zero hn
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
exact hlogb_nonneg
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ⌊(↑b).logb ↑n⌋₊ ≤ b.log n
Tactic:
apply Nat.le_log_of_pow_le hb
Proof state after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ ⌊(↑b).logb ↑n⌋₊ ≤ n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n
Tactic:
rw [← Real.rpow_natCast]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n
Tactic:
gcongr
Proof state after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ ↑b

case hyz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑⌊(↑b).logb ↑n⌋₊ ≤ (↑b).logb ↑n
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hyz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑⌊(↑b).logb ↑n⌋₊ ≤ (↑b).logb ↑n
Tactic:
apply Nat.floor_le hlogb_nonneg
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ ↑b
Tactic:
norm_cast
Proof state after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ b
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ b
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ (↑b).logb ↑n = ↑n
Tactic:
rw [Real.rpow_logb] <;> norm_cast <;> omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
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:
intro n
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (Finset.range N) →
    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))
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (Finset.range N) →
    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:
simp only [Finset.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_union, Finset.mem_image,
  Finset.mem_product, Prod.exists, and_imp]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → IsPrimePow n → n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → IsPrimePow n → n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
intro hnN hnprime
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
rcases prime_or_pow N n hnN hnprime with hp | ⟨m, hm, k, hk, h⟩
Proof state after:
case inl
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

case inr.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case inl
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
left
Proof state after:
case inl.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case inl.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime
Tactic:
exact ⟨hnN, hp⟩
Proof state after:
no goals
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case inr.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
right
Proof state after:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
refine ⟨m, k, ?_⟩
Proof state after:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
by_cases hm : m = 0
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
rw [Nat.lt_ceil, Nat.lt_succ_iff]
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Tactic:
have : 1 ≤ m := by omega
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
this : 1 ≤ m
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
this : 1 ≤ m
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Tactic:
aesop
Proof state after:
no goals
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
rw [hm, zero_pow] at h
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Tactic:
exact False.elim (hnprime.ne_zero h)
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Tactic:
rintro rfl
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 0 ^ 0
⊢ False
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 0 ^ 0
⊢ False
Tactic:
simp only [pow_zero] at h
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 1
⊢ False
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 1
⊢ False
Tactic:
exact False.elim (hnprime.ne_one h)
Proof state after:
no goals
Theorem: BrunTitchmarsh.range_filter_isPrimePow_subset_union
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ 1 ≤ m
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ f =O[⊤] g
Tactic:
simp only [Asymptotics.isBigO_top, Real.norm_eq_abs]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
rw [Asymptotics.isBigO_atTop_iff_eventually_exists] at h
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : ∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : ∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
simp only [ge_iff_le, Real.norm_eq_abs, Filter.eventually_atTop] at h
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
obtain ⟨N, hN⟩ := h
Proof state after:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
specialize hN N le_rfl
Proof state after:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∃ c, ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∃ c, ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
obtain ⟨c, hc⟩ := hN
Proof state after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|