Theorem: PNT_vonMangoldt (EulerProducts/PNT.lean)

State before:
WIT : WienerIkeharaTheorem
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)
Tactic:
have hnv := riemannZeta_ne_zero_of_one_le_re
State after:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)

State before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)
Tactic:
refine WIT (F := fun z ↦ -deriv ζ₁ z / ζ₁ z) (fun _ ↦ vonMangoldt_nonneg) (fun s hs ↦ ?_) ?_
State after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s

case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {s | 1 ≤ s.re}

State before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s
Tactic:
have hs₁ : s ≠ 1 := by
  rintro rfl
  simp at hs
State after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s

State before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s
Tactic:
simp only [ne_eq, hs₁, not_false_eq_true, LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs,
  ofReal_one]
State after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ -deriv ζ₁ s / ζ₁ s = -deriv ζ s / ζ s - 1 / (s - 1)

State before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ -deriv ζ₁ s / ζ₁ s = -deriv ζ s / ζ s - 1 / (s - 1)
Tactic:
exact neg_logDeriv_ζ₁_eq hs₁ <| hnv hs₁ (Set.mem_setOf.mp hs).le
State after:
no goals

State before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ s ≠ 1
Tactic:
rintro rfl
State after:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
hs : 1 ∈ {s | 1 < s.re}
⊢ False

State before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
hs : 1 ∈ {s | 1 < s.re}
⊢ False
Tactic:
simp at hs
State after:
no goals

State before:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {s | 1 ≤ s.re}
Tactic:
refine continuousOn_neg_logDeriv_ζ₁.mono fun s _ ↦ ?_
State after:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}

State before:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
specialize @hnv s
State after:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
hnv : s ≠ 1 → 1 ≤ s.re → ζ s ≠ 0
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}

State before:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
hnv : s ≠ 1 → 1 ≤ s.re → ζ s ≠ 0
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
simp at *
State after:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : 1 ≤ s.re
hnv : ¬s = 1 → 1 ≤ s.re → ¬ζ s = 0
⊢ s = 1 ∨ ¬ζ s = 0

State before:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : 1 ≤ s.re
hnv : ¬s = 1 → 1 ≤ s.re → ¬ζ s = 0
⊢ s = 1 ∨ ¬ζ s = 0
Tactic:
tauto
State after:
no goals