noncomputable def MultiplicativeConvolution.mulConv_ZMod (q : ℕ) [NeZero q] (f g : ZMod q → ℂ) (a : ZMod q) : ℂ

Multiplicative convolution on ZMod q: $(f *_M g)(a) = \sum_{b, c \in \mathbb{Z}/q,\ bc = a} f(b)\, g(c)$.

noncomputable def MultiplicativeConvolution.modProjection_arith (N q : ℕ) [NeZero q] (f : ℕ → ℂ) (a : ZMod q) : ℂ

The projection $\pi_q f : \mathbb{Z}/q \to \mathbb{C}$ of an arithmetic function $f : \mathbb{N} \to \mathbb{C}$ truncated to $[0, N)$: at $a \in \mathbb{Z}/q$ it sums $f(n)$ over $n < N$ with $n \equiv a \pmod q$.

theorem MultiplicativeConvolution.sum_comm4 (N q : ℕ) [NeZero q] (h : ZMod q → ZMod q → ℕ → ℕ → ℂ) : ∑ b : ZMod q, ∑ c : ZMod q, ∑ n ∈ Finset.range N, ∑ m ∈ Finset.range N, h b c n m = ∑ n ∈ Finset.range N, ∑ m ∈ Finset.range N, ∑ b : ZMod q, ∑ c : ZMod q, h b c n m

Swap the order of four nested sums (two over ZMod q, two over Finset.range N) so that the n, m sums are outermost — used to rearrange double sums in the projection-of-convolution computation.

theorem MultiplicativeConvolution.mulConv_ZMod_eq_double_sum (N q : ℕ) [NeZero q] (f g : ℕ → ℂ) (a : ZMod q) : mulConv_ZMod q (modProjection_arith N q f) (modProjection_arith N q g) a = ∑ n ∈ Finset.range N, ∑ m ∈ Finset.range N, if ↑n * ↑m = a then f n * g m else 0

Expanding the mod-$q$ multiplicative convolution of two truncated projections: $\bigl(\pi_q f *_M \pi_q g\bigr)(a) = \sum_{n, m < N,\ nm \equiv a} f(n)\, g(m)$.

theorem MultiplicativeConvolution.sum_product_eq_sum_divisorsAntidiagonal (N : ℕ) (f g : ℕ → ℂ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (hg : ∀ (n : ℕ), N ≤ n → g n = 0) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (n : ℕ) (hn : n < N * N) : ∑ x ∈ Finset.range N ×ˢ Finset.range N with x.1 * x.2 = n, f x.1 * g x.2 = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2

If $f, g$ are supported on positive integers $< N$, then for $n < N^2$ the truncated product-sum $\sum_{(d_1, d_2) \in [0,N)^2,\ d_1 d_2 = n} f(d_1) g(d_2)$ equals the sum over the full divisor antidiagonal $\sum_{d_1 d_2 = n} f(d_1) g(d_2)$.

theorem MultiplicativeConvolution.modProjection_mulConv (N q : ℕ) [NeZero q] (f g : ℕ → ℂ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (hg : ∀ (n : ℕ), N ≤ n → g n = 0) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (a : ZMod q) : modProjection_arith (N * N) q (mulConv f g) a = mulConv_ZMod q (modProjection_arith N q f) (modProjection_arith N q g) a

Projection of multiplicative convolution (pointwise form): if $f, g$ are supported on positive integers $< N$, then $\pi_q(f *_M g)(a) = (\pi_q f *_M \pi_q g)(a)$, where the truncation on the left is taken at $N^2$.

theorem MultiplicativeConvolution.modProjection_mulConv_arithFun (N q : ℕ) [NeZero q] (f g : ArithmeticFunction ℂ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (hg : ∀ (n : ℕ), N ≤ n → g n = 0) (a : ZMod q) : modProjection_arith (N * N) q (fun (n : ℕ) => (f * g) n) a = mulConv_ZMod q (modProjection_arith N q ⇑f) (modProjection_arith N q ⇑g) a

Projection-of-convolution identity for ArithmeticFunctions: with the support hypotheses on $f, g$, we have $\pi_q(f * g)(a) = (\pi_q f *_M \pi_q g)(a)$ (here f * g is Dirichlet convolution of arithmetic functions).

theorem MultiplicativeConvolution.modProjection_mulConv_arithFun' (N q : ℕ) [NeZero q] (f g : ℕ → ℂ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (hg : ∀ (n : ℕ), N ≤ n → g n = 0) (hf0 : f 0 = 0) (hg0 : g 0 = 0) : modProjection_arith (N * N) q (mulConv f g) = mulConv_ZMod q (modProjection_arith N q f) (modProjection_arith N q g)

Functional form of the projection-of-convolution identity: under the support hypotheses, $\pi_q(f *_M g) = \pi_q f *_M \pi_q g$ as functions on $\mathbb{Z}/q$.

noncomputable def MultiplicativeConvolution.modProjection_pos (N q : ℕ) [NeZero q] (f : ℕ → ℂ) (a : ZMod q) : ℂ

The mod-$q$ projection of $f$ on $\mathbb{N}$ truncated to $1 \le n < N$ (positive integers only): $\pi_q^+ f(a) = \sum_{0 < n < N,\ n \equiv a} f(n)$.

def MultiplicativeConvolution.zeroAt0 (f : ℕ → ℂ) : ℕ → ℂ

Modify $f : \mathbb{N} \to \mathbb{C}$ so that its value at $0$ is set to $0$, leaving all other values unchanged.

theorem MultiplicativeConvolution.zeroAt0_zero (f : ℕ → ℂ) : zeroAt0 f 0 = 0

zeroAt0 f vanishes at $0$.

theorem MultiplicativeConvolution.zeroAt0_support (f : ℕ → ℂ) (N : ℕ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (n : ℕ) : N ≤ n → zeroAt0 f n = 0

If $f$ is supported on $n < N$, so is zeroAt0 f.

theorem MultiplicativeConvolution.modProjection_pos_eq_arith_zeroAt0 (N q : ℕ) [NeZero q] (f : ℕ → ℂ) (a : ZMod q) : modProjection_pos N q f a = modProjection_arith N q (zeroAt0 f) a

The positive-truncation projection equals the arithmetic projection of $f$ with its value at $0$ zeroed out: $\pi_q^+ f = \pi_q (\mathrm{zeroAt0}\, f)$.

theorem MultiplicativeConvolution.mulConv_pos_eq_zeroAt0 (f g : ℕ → ℂ) (n : ℕ) (hn : n ≠ 0) : mulConv f g n = mulConv (zeroAt0 f) (zeroAt0 g) n

For $n \ne 0$, the multiplicative convolution $(f *_M g)(n)$ is unchanged if we replace $f, g$ by their zeroAt0 modifications (the value at $0$ does not contribute when $n > 0$).

theorem MultiplicativeConvolution.modProjection_mulConv_pos (N q : ℕ) [NeZero q] (f g : ℕ → ℂ) (hf : ∀ (n : ℕ), N ≤ n → f n = 0) (hg : ∀ (n : ℕ), N ≤ n → g n = 0) : modProjection_pos (N * N) q (mulConv f g) = mulConv_ZMod q (modProjection_pos N q f) (modProjection_pos N q g)

Projection of multiplicative convolution (positive-truncation version): if $f, g$ are supported on $n < N$, then $\pi_q^+(f *_M g) = \pi_q^+ f *_M \pi_q^+ g$ as functions on $\mathbb{Z}/q$.