convolution_def — Mathlib

English

Explicit expression for Dirichlet convolution: (f ⍟ g)(n) = ∑_{p ∈ n.divisorsAntidiagonal} f(p1) g(p2).

Русский

Явное выражение дирихлетовой свёртки: (f ⍟ g)(n) = ∑_{p ∈ n.divisorsAntidiagonal} f(p1) g(p2).

LaTeX

$$$f \\star g = \\lambda n. \\sum_{p \\in n.divisorsAntidiagonal} f(p.1) \\; g(p.2).$$$

Lean4

theorem convolution_def {R : Type*} [Semiring R] (f g : ℕ → R) :
    f ⍟ g = fun n ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2 :=
  by
  ext n
  simpa [convolution, toArithmeticFunction] using
    Finset.sum_congr rfl fun p hp ↦ by simp [ne_zero_of_mem_divisorsAntidiagonal hp]

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