Theorem: WeakPNT (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have hnv := riemannZeta_ne_zero_of_one_le_re
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l1 (n : ℕ) : 0 ≤ Λ n := vonMangoldt_nonneg
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l2 s (hs : 1 < s.re) : (-deriv ζ₁ / ζ₁) s = LSeries Λ s - 1 / (s - 1) := by
  have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
  simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re} := continuousOn_neg_logDeriv_ζ₁.mono (by tauto)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l4 : cheby Λ := vonMangoldt_cheby
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by
  simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
l5 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(Λ n)) σ')
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
l5 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(Λ n)) σ')
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
apply WienerIkeharaTheorem' l1 l5 l4 l3 l2
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
Tactic:
have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
hs₁ : s ≠ 1
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
hs₁ : s ≠ 1
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
Tactic:
simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
⊢ s ≠ 1
Tactic:
contrapose! hs
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : s = 1
⊢ s.re ≤ 1

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : s = 1
⊢ s.re ≤ 1
Tactic:
simp [hs]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ {s | 1 ≤ s.re} ⊆ {z | z = 1 ∨ riemannZeta z ≠ 0}
Tactic:
tauto
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
σ' : ℝ
hσ' : 1 < σ'
⊢ Summable (nterm (fun n => ↑(Λ n)) σ')
Tactic:
simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
State after:
no goals