Theorem: vonMangoldt_cheby (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ cheby fun n => ↑(Λ n)
Tactic:
obtain ⟨C, hC⟩ := BrunTitchmarsh.card_range_filter_isPrimePow_le
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
⊢ cheby fun n => ↑(Λ n)

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
⊢ cheby fun n => ↑(Λ n)
Tactic:
have hC_nonneg : 0 ≤ C := by
  have := hC 2
  norm_cast at this
  have hpos : 0 < 2 / Real.log 2 := by positivity
  rw [← mul_le_mul_right hpos]
  linarith
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
⊢ cheby fun n => ↑(Λ n)

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
⊢ cheby fun n => ↑(Λ n)
Tactic:
use C
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
⊢ chebyWith C fun n => ↑(Λ n)

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
⊢ chebyWith C fun n => ↑(Λ n)
Tactic:
intro n
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ cumsum (fun x => ‖(fun n => ↑(Λ n)) x‖) n ≤ C * ↑n

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
⊢ 0 ≤ C
Tactic:
have := hC 2
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (↑2 / (↑2).log)
⊢ 0 ≤ C

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (↑2 / (↑2).log)
⊢ 0 ≤ C
Tactic:
norm_cast at this
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
⊢ 0 ≤ C

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
⊢ 0 ≤ C
Tactic:
have hpos : 0 < 2 / Real.log 2 := by positivity
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 ≤ C

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 ≤ C
Tactic:
rw [← mul_le_mul_right hpos]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 * (2 / Real.log 2) ≤ C * (2 / Real.log 2)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 * (2 / Real.log 2) ≤ C * (2 / Real.log 2)
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
⊢ 0 < 2 / Real.log 2
Tactic:
positivity
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ x ∈ Finset.range n, (fun x => ‖(fun n => ↑(Λ n)) x‖) x = Λ x
Tactic:
simp
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ i ∈ Finset.range n, Λ i ≤ ∑ i ∈ Finset.range n, if IsPrimePow i then (↑i).log else 0
Tactic:
apply Finset.sum_le_sum
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i ∈ Finset.range n, Λ i ≤ if IsPrimePow i then (↑i).log else 0

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i ∈ Finset.range n, Λ i ≤ if IsPrimePow i then (↑i).log else 0
Tactic:
intro i _
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ Λ i ≤ if IsPrimePow i then (↑i).log else 0

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ Λ i ≤ if IsPrimePow i then (↑i).log else 0
Tactic:
rw [ArithmeticFunction.vonMangoldt_apply]
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ (if IsPrimePow i then (↑i.minFac).log else 0) ≤ if IsPrimePow i then (↑i).log else 0

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ (if IsPrimePow i then (↑i.minFac).log else 0) ≤ if IsPrimePow i then (↑i).log else 0
Tactic:
split_ifs with h
State after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
⊢ (↑i.minFac).log ≤ (↑i).log

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : ¬IsPrimePow i
⊢ 0 ≤ 0

State before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
⊢ (↑i.minFac).log ≤ (↑i).log
Tactic:
have := (Nat.minFac_prime (h.ne_one)).pos
State after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
this : 0 < i.minFac
⊢ (↑i.minFac).log ≤ (↑i).log

State before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
this : 0 < i.minFac
⊢ (↑i.minFac).log ≤ (↑i).log
Tactic:
gcongr
State after:
case pos.hxy.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
this : 0 < i.minFac
⊢ i.minFac ≤ i

State before:
case pos.hxy.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
this : 0 < i.minFac
⊢ i.minFac ≤ i
Tactic:
apply Nat.minFac_le h.pos
State after:
no goals

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : ¬IsPrimePow i
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ (∑ i ∈ Finset.range n, if IsPrimePow i then (↑i).log else 0) ≤
    ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log
Tactic:
rw [← Finset.sum_filter]
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ a ∈ Finset.filter (fun i => IsPrimePow i) (Finset.range n), (↑a).log ≤
    ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ a ∈ Finset.filter (fun i => IsPrimePow i) (Finset.range n), (↑a).log ≤
    ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log
Tactic:
apply Finset.sum_le_sum
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i ∈ Finset.filter (fun i => IsPrimePow i) (Finset.range n), (↑i).log ≤ (↑n).log

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i ∈ Finset.filter (fun i => IsPrimePow i) (Finset.range n), (↑i).log ≤ (↑n).log
Tactic:
simp only [Finset.mem_filter, Finset.mem_range, and_imp]
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i < n, IsPrimePow i → (↑i).log ≤ (↑n).log

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i < n, IsPrimePow i → (↑i).log ≤ (↑n).log
Tactic:
intro i hi hi_p
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
⊢ (↑i).log ≤ (↑n).log

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
⊢ (↑i).log ≤ (↑n).log
Tactic:
have := hi_p.pos
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
this : 0 < i
⊢ (↑i).log ≤ (↑n).log

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
this : 0 < i
⊢ (↑i).log ≤ (↑n).log
Tactic:
gcongr
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log
Tactic:
simp
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card * (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card * (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log
Tactic:
gcongr
State after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card ≤ C * (↑n / (↑n).log)

State before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card ≤ C * (↑n / (↑n).log)
Tactic:
apply hC
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
by_cases hn : n = 0
State after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
by_cases hn1 : n = 1
State after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
have : 0 < Real.log n := by
  apply Real.log_pos
  norm_cast
  omega
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
this : 0 < (↑n).log
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
this : 0 < (↑n).log
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
field_simp
State after:
no goals

State before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
simp [hn]
State after:
no goals

State before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
simp [hn1, hC_nonneg]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 0 < (↑n).log
Tactic:
apply Real.log_pos
State after:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < ↑n

State before:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < ↑n
Tactic:
norm_cast
State after:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < n

State before:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < n
Tactic:
omega
State after:
no goals