internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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
Proof 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
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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
Proof 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
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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)]
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_pows_aux
Proof 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]
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N
Tactic:
norm_num
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[atTop] fun 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))).card
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 IsPrimePow (Finset.range x)).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter IsPrimePow (Finset.range x)).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Tactic:
simp only [RCLike.norm_natCast, Nat.cast_le]
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    (Finset.filter IsPrimePow (Finset.range x)).card ≤
      (Finset.filter Nat.Prime (Finset.range x) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    (Finset.filter IsPrimePow (Finset.range x)).card ≤
      (Finset.filter Nat.Prime (Finset.range x) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card
Tactic:
intro N
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter IsPrimePow (Finset.range N)).card ≤
    (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))).card
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter IsPrimePow (Finset.range N)).card ≤
    (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))).card
Tactic:
apply Finset.card_le_card
Proof state after:
case hfg.a
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))
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case hfg.a
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:
apply range_filter_isPrimePow_subset_union
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun N =>
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
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) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
Tactic:
simp only [RCLike.norm_natCast, Real.norm_eq_abs]
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) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card ≤
      |↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card|
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
            Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card ≤
      |↑(Finset.filter Nat.Prime (Finset.range x)).card +
          ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card|
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) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    |↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card|
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    |↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card|
Tactic:
rw [abs_of_nonneg (by positivity)]
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) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
norm_cast
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) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.filter Nat.Prime (Finset.range N)).card +
      (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Theorem: BrunTitchmarsh.card_isPrimePow_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) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.filter Nat.Prime (Finset.range N)).card +
      (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
apply Finset.card_union_le
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤
    ↑(Finset.filter Nat.Prime (Finset.range N)).card +
      ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card
Tactic:
positivity
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_isPrimePow_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 +
        ↑(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.add
Proof state after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.filter Nat.Prime (Finset.range x)).card) =O[atTop] fun N => ↑N / (↑N).log

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
Tactic:
apply card_pows_aux
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_isPrimePow_isBigO
Proof state before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.filter Nat.Prime (Finset.range x)).card) =O[atTop] fun N => ↑N / (↑N).log
Tactic:
exact card_range_filter_prime_isBigO
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
Tactic:
convert_to (fun N ↦ ((Finset.range N).filter IsPrimePow).card : ℕ → ℝ) =O[⊤] (fun N ↦ (N / Real.log N))
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
Tactic:
apply IsBigO.nat_Top_of_atTop _ _ card_isPrimePow_isBigO
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (n : ℕ), ↑n / (↑n).log = 0 → ↑(Finset.filter IsPrimePow (Finset.range n)).card = 0
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (n : ℕ), ↑n / (↑n).log = 0 → ↑(Finset.filter IsPrimePow (Finset.range n)).card = 0
Tactic:
simp only [div_eq_zero_iff, Nat.cast_eq_zero, Real.log_eq_zero, Nat.cast_eq_one, or_self_left,
  Finset.card_eq_zero, forall_eq_or_imp, Finset.range_zero, Finset.filter_empty, Finset.range_one,
  true_and]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter IsPrimePow {0} = ∅ ∧ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter IsPrimePow {0} = ∅ ∧ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
refine ⟨rfl, ?_⟩
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
intro a ha
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ Finset.filter IsPrimePow (Finset.range a) = ∅
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ Finset.filter IsPrimePow (Finset.range a) = ∅
Tactic:
exfalso
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ False
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ False
Tactic:
linarith [show 0 ≤ (a : ℝ) by positivity]
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
Tactic:
simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs]
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    ∃ C, ∀ (x : ℕ), ↑(Finset.filter IsPrimePow (Finset.range x)).card ≤ C * (↑x / |(↑x).log|)
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    ∃ C, ∀ (x : ℕ), ↑(Finset.filter IsPrimePow (Finset.range x)).card ≤ C * (↑x / |(↑x).log|)
Tactic:
peel with C N
Proof state after:
case a.h.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case a.h.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
by_cases hN : N = 0
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
rw [abs_of_nonneg]
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ (↑N).log
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ (↑N).log
Tactic:
apply Real.log_nonneg
Proof state after:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ↑N
Tactic:
norm_cast
Proof state after:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case neg.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ N
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
Tactic:
simp [hN]
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_range_filter_isPrimePow_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ 0 ≤ ↑a
Tactic:
positivity
Proof state after:
no goals
Theorem: Sieve.selbergTerms_apply
Proof state before:
s : Sieve
d : ℕ
⊢ g d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
unfold selbergTerms
Proof state after:
s : Sieve
d : ℕ
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_apply
Proof state before:
s : Sieve
d : ℕ
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
by_cases h : d=0
Proof state after:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)

case neg
s : Sieve
d : ℕ
h : ¬d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_apply
Proof state before:
case neg
s : Sieve
d : ℕ
h : ¬d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
rw [ArithmeticFunction.pmul_apply, ArithmeticFunction.prodPrimeFactors_apply h]
Proof state after:
no goals
Theorem: Sieve.selbergTerms_apply
Proof state before:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
rw [h]
Proof state after:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) 0 = ν 0 * ∏ p ∈ primeFactors 0, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_apply
Proof state before:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) 0 = ν 0 * ∏ p ∈ primeFactors 0, 1 / (1 - ν p)
Tactic:
simp
Proof state after:
no goals
Theorem: Sieve.squarefree_of_mem_divisors_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ Squarefree d
Tactic:
simp only [Nat.mem_divisors] at hd
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ Squarefree d
Theorem: Sieve.squarefree_of_mem_divisors_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ Squarefree d
Tactic:
exact Squarefree.squarefree_of_dvd hd.left s.prodPrimes_squarefree
Proof state after:
no goals
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d
Tactic:
calc
  0 < ∏ p in d.primeFactors, ν p := by
    apply prod_pos
    intro p hpd
    have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
    have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd
    exact s.nu_pos_of_prime p hp_prime hp_dvd
  _ = ν d := s.nu_mult.prod_factors_of_mult ν (Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree)
Proof state after:
no goals
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ∏ p ∈ d.primeFactors, ν p
Tactic:
apply prod_pos
Proof state after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ i ∈ d.primeFactors, 0 < ν i
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ i ∈ d.primeFactors, 0 < ν i
Tactic:
intro p hpd
Proof state after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < ν p
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < ν p
Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
Proof state after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
⊢ 0 < ν p
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
⊢ 0 < ν p
Tactic:
have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd
Proof state after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < ν p
Theorem: Sieve.nu_pos_of_dvd_prodPrimes
Proof state before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < ν p
Tactic:
exact s.nu_pos_of_prime p hp_prime hp_dvd
Proof state after:
no goals
Theorem: Sieve.nu_ne_zero
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ν d ≠ 0
Tactic:
apply _root_.ne_of_gt
Proof state after:
case h
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d
Theorem: Sieve.nu_ne_zero
Proof state before:
case h
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d
Tactic:
exact nu_pos_of_dvd_prodPrimes s hd
Proof state after:
no goals