convolution — Mathlib

English

Dirichlet convolution of f and g is defined by (f ⍟ g)(n) = ∑_{p ∈ n.divisorsAntidiagonal} f(p1) g(p2).

Русский

Дирихлетова свёртка двух последовательностей определяется как (f ⍟ g)(n) = ∑_{p ∈ n.divisorsAntidiagonal} f(p1) g(p2).

LaTeX

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

Lean4

/-- Dirichlet convolution of two sequences.

We define this in terms of the already existing definition for arithmetic functions. -/
noncomputable def convolution {R : Type*} [Semiring R] (f g : ℕ → R) : ℕ → R :=
  ⇑(toArithmeticFunction f * toArithmeticFunction g)

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