convolution_vonMangoldt_zeta — Mathlib

English

The Dirichlet convolution of the von Mangoldt function Λ with the constant function 1 equals the logarithm function: (Λ * 1)(n) = log n for all n ≥ 1. Equivalently, ∑_{d|n} Λ(d) = log n.

Русский

Свёртка Дирихле функции фон Маннглотта Λ с константой 1 равна логарифмической функции: (Λ * 1)(n) = log n для всех n ≥ 1; эквивалентно сумме по делителям ∑_{d|n} Λ(d) = log n.

LaTeX

$$$(\\Lambda * 1)(n) = \\log n \\quad \\text{для всех } n \\ge 1$$$

Lean4

/-- A translation of the relation `Λ * ↑ζ = log` of (real-valued) arithmetic functions
to an equality of complex sequences. -/
theorem convolution_vonMangoldt_zeta : ↗Λ ⍟ ↗ζ = ↗Complex.log :=
  by
  ext n
  simpa [apply_ite, LSeries.convolution_def, -vonMangoldt_mul_zeta] using congr_arg (ofReal <| · n) vonMangoldt_mul_zeta

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