not_LSeriesSummable_moebius_at_one

English

The L-series of the Moebius function at s = 1 is not summable.

Русский

L‑серия Моебиуса в s = 1 не суммируема.

LaTeX

$$¬ LSeriesSummable (↗μ) 1$$

Lean4

theorem not_LSeriesSummable_moebius_at_one : ¬LSeriesSummable (↗μ) 1 :=
  by
  refine fun h ↦ not_summable_one_div_on_primes <| summable_ofReal.mp <| .of_neg ?_
  refine (h.indicator {n | n.Prime}).congr fun n ↦ ?_
  by_cases hn : n.Prime
  · simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]
  · simp [hn]

Похожие утверждения