noncomputable def HighFreqMultConv.mulConvUnits (q : ℕ) [NeZero q] (f g : (ZMod q)ˣ → ℂ) (a : (ZMod q)ˣ) : ℂ

The multiplicative convolution on the group of units (ZMod q)ˣ: $(f *_M g)(a) = \sum_{b \in (\mathbb{Z}/q)^\times} f(b)\, g(a/b)$.

noncomputable def HighFreqMultConv.highFreqUnits (q : ℕ) [NeZero q] (f : (ZMod q)ˣ → ℂ) (a : (ZMod q)ˣ) : ℂ

The high-frequency part f_h = f - f₀ of a function on (ZMod q)ˣ, where f₀ is the constant function equal to the average $\langle f \rangle = \frac{1}{|(\mathbb{Z}/q)^\times|}\sum_b f(b)$.

theorem HighFreqMultConv.sum_div_left_eq (q : ℕ) [NeZero q] (g : (ZMod q)ˣ → ℂ) (a : (ZMod q)ˣ) : ∑ b : (ZMod q)ˣ, g (a / b) = ∑ b : (ZMod q)ˣ, g b

Translation invariance from the left: summing g(a/b) over b gives the same answer as summing g(b) over b, since b ↦ a/b is a bijection of (ZMod q)ˣ.

theorem HighFreqMultConv.sum_div_right_eq (q : ℕ) [NeZero q] (g : (ZMod q)ˣ → ℂ) (x : (ZMod q)ˣ) : ∑ i : (ZMod q)ˣ, g (i / x) = ∑ i : (ZMod q)ˣ, g i

Translation invariance from the right: summing g(i/x) over i equals ∑ g(i).

theorem HighFreqMultConv.highFreq_mulConvUnits (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f g : (ZMod q)ˣ → ℂ) : highFreqUnits q (mulConvUnits q f g) = mulConvUnits q (highFreqUnits q f) (highFreqUnits q g)

High-frequency part of a multiplicative convolution (Lemma 4 in Section 7.3). On (ZMod q)ˣ, taking the high-frequency part commutes with multiplicative convolution: $(f^* *_M g^*)_h = f^*_h *_M g^*_h$.