noncomputable def HighFreqMultConv.l2NormUnits (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f : (ZMod q)ˣ → ℂ) : ℝ

The $L^2$ norm of $f : (\mathbb{Z}/q)^* \to \mathbb{C}$ on the unit group, $\|f\|_{L^2((\mathbb{Z}/q)^*)} = \bigl(\sum_{b \in (\mathbb{Z}/q)^*} |f(b)|^2\bigr)^{1/2}$.

theorem HighFreqMultConv.mulConvUnits_eq_mulConv (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f g : (ZMod q)ˣ → ℂ) (a : (ZMod q)ˣ) : mulConvUnits q f g a = MultiplicativeConvolution.mulConv f g a

The multiplicative convolution on units mulConvUnits agrees pointwise with the generic multiplicative convolution MultiplicativeConvolution.mulConv on the unit group.

theorem HighFreqMultConv.l2NormUnits_eq_l2Norm (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f : (ZMod q)ˣ → ℂ) : l2NormUnits q f = MultiplicativeConvolution.l2Norm f

The unit-group $L^2$ norm l2NormUnits agrees with the generic l2Norm from MultiplicativeConvolution.

theorem HighFreqMultConv.norm_highFreq_mulConvUnits_le (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f g : (ZMod q)ˣ → ℂ) (a : (ZMod q)ˣ) : ‖highFreqUnits q (mulConvUnits q f g) a‖ ≤ l2NormUnits q (highFreqUnits q f) * l2NormUnits q (highFreqUnits q g)

Pointwise high-frequency $L^\infty$ bound on the multiplicative convolution: for every $a \in (\mathbb{Z}/q)^*$, $|(f *_M g)_h(a)| \le \|f_h\|_{L^2((\mathbb{Z}/q)^*)} \, \|g_h\|_{L^2((\mathbb{Z}/q)^*)}$.

theorem HighFreqMultConv.highFreq_mulConv_linfty_le_l2_l2 (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (f g : (ZMod q)ˣ → ℂ) : ⨆ (a : (ZMod q)ˣ), ‖highFreqUnits q (mulConvUnits q f g) a‖ ≤ l2NormUnits q (highFreqUnits q f) * l2NormUnits q (highFreqUnits q g)

Multiplicative convolution $L^\infty$ bound on the units (high-frequency part): $\|(f *_M g)_h\|_{L^\infty((\mathbb{Z}/q)^*)} \le \|f_h\|_{L^2} \, \|g_h\|_{L^2}$.

def HighFreqMultConv.restrictToUnits (q : ℕ) [Fact (Nat.Prime q)] (F : ZMod q → ℂ) : (ZMod q)ˣ → ℂ

Restrict a function $F : \mathbb{Z}/q \to \mathbb{C}$ to the unit group $(\mathbb{Z}/q)^*$ by composing with the natural map $u \mapsto (u : \mathbb{Z}/q)$.

noncomputable def HighFreqMultConv.l2Norm_ZMod (q : ℕ) [NeZero q] (F : ZMod q → ℂ) : ℝ

The $L^2$ norm of $F : \mathbb{Z}/q \to \mathbb{C}$, $\|F\|_{L^2(\mathbb{Z}/q)} = \bigl(\sum_{a} |F(a)|^2\bigr)^{1/2}$.

theorem HighFreqMultConv.mulConv_ZMod_units_eq_mulConvUnits (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (F G : ZMod q → ℂ) (u : (ZMod q)ˣ) : MultiplicativeConvolution.mulConv_ZMod q F G ↑u = mulConvUnits q (restrictToUnits q F) (restrictToUnits q G) u

For $u \in (\mathbb{Z}/q)^*$, the mod-$q$ multiplicative convolution of $F, G : \mathbb{Z}/q \to \mathbb{C}$ evaluated at $u$ agrees with the unit-group multiplicative convolution of the restrictions $F|_{(\mathbb{Z}/q)^*}$ and $G|_{(\mathbb{Z}/q)^*}$.

theorem HighFreqMultConv.restrictToUnits_mulConv_ZMod_eq (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (F G : ZMod q → ℂ) : restrictToUnits q (MultiplicativeConvolution.mulConv_ZMod q F G) = mulConvUnits q (restrictToUnits q F) (restrictToUnits q G)

Functional form: restricting the mod-$q$ multiplicative convolution of $F, G$ to the unit group equals the unit-group multiplicative convolution of the restrictions.

theorem HighFreqMultConv.l2NormUnits_highFreq_restrict_le (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (F : ZMod q → ℂ) : l2NormUnits q (highFreqUnits q (restrictToUnits q F)) ≤ l2Norm_ZMod q (LinnikLargeSieve.highFreqPart_ZMod q F)

Comparison of $L^2$ norms of high-frequency parts: $\|(F^*)_h\|_{L^2((\mathbb{Z}/q)^*)} \le \|F_h\|_{L^2(\mathbb{Z}/q)}$, where $F^*$ is the restriction of $F$ to the unit group. This is Lemma 3 from §7.3 of the textbook.

theorem HighFreqMultConv.highFreq_mulConv_linfty_le_l2_l2_full (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (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) : ⨆ (a : (ZMod q)ˣ), ‖highFreqUnits q (restrictToUnits q (MultiplicativeConvolution.mulConv_ZMod q (MultiplicativeConvolution.modProjection_arith N q f) (MultiplicativeConvolution.modProjection_arith N q g))) a‖ ≤ l2Norm_ZMod q (LinnikLargeSieve.highFreqPart_ZMod q (MultiplicativeConvolution.modProjection_arith N q f)) * l2Norm_ZMod q (LinnikLargeSieve.highFreqPart_ZMod q (MultiplicativeConvolution.modProjection_arith N q g))

Full-version $L^\infty$ bound: for $f, g : \mathbb{N} \to \mathbb{C}$ supported on $[1, N)$, $$\|(\pi_q(f *_M g))^*_h\|_{L^\infty((\mathbb{Z}/q)^*)} \le \|(\pi_q f)_h\|_{L^2(\mathbb{Z}/q)} \, \|(\pi_q g)_h\|_{L^2(\mathbb{Z}/q)},$$ where the left side is the high-frequency part on units of the projection of the multiplicative convolution.