LSeries_zeta_mul_Lseries_moebius — Mathlib

English

For Re(s) > 1, the L-series of the constant function 1 and the L-series of the Möbius function μ are inverses: L((↗ζ), s) · L((↗μ), s) = 1.

Русский

Пусть Re(s) > 1. Тогда L-серия константы 1 и L-серия функции Моебиуса μ являются об inverses: L((↗ζ), s) · L((↗μ), s) = 1.

LaTeX

$$$1 < \\operatorname{Re}(s) \\Rightarrow L(↗ζ,s) \\cdot L(↗μ,s) = 1$$$

Lean4

/-- The L-series of the arithmetic function `ζ` and of the Möbius function are inverses. -/
theorem LSeries_zeta_mul_Lseries_moebius {s : ℂ} (hs : 1 < s.re) : L (↗ζ) s * L (↗μ) s = 1 :=
  by
  rw [← LSeries_convolution' (LSeriesSummable_zeta_iff.mpr hs) (LSeriesSummable_moebius_iff.mpr hs)]
  simp [← natCoe_apply, ← intCoe_apply, coe_mul, one_eq_delta, LSeries_delta, -zeta_apply]

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