noncomputable def MultiplicativeConvolution.mulConv {G : Type u_1} [Fintype G] [Group G] (f g : G → ℂ) (a : G) : ℂ

Multiplicative (group) convolution of two functions f, g : G → ℂ on a finite group G, defined by (f *_M g)(a) = ∑_{b ∈ G} f(b) · g(a · b⁻¹).

noncomputable def MultiplicativeConvolution.l2Norm {G : Type u_1} [Fintype G] (f : G → ℂ) : ℝ

The $L^2$ norm of a function f : G → ℂ on a finite group, i.e. ‖f‖₂ = √(∑_b ‖f b‖²).

def MultiplicativeConvolution.mulInvEquiv {G : Type u_1} [Group G] (a : G) : G ≃ G

For a fixed a ∈ G, the map b ↦ a · b⁻¹ is a bijection of G to itself. This is used to reindex sums in convolution estimates.

theorem MultiplicativeConvolution.norm_mulConv_le {G : Type u_1} [Fintype G] [Group G] (f g : G → ℂ) (a : G) : ‖mulConv f g a‖ ≤ l2Norm f * l2Norm g

Pointwise bound on multiplicative convolution: by Cauchy–Schwarz, ‖(f *_M g)(a)‖ ≤ ‖f‖₂ · ‖g‖₂ for every a ∈ G.

theorem MultiplicativeConvolution.linftyNorm_mulConv_le {G : Type u_1} [Fintype G] [Group G] (f g : G → ℂ) : ⨆ (a : G), ‖mulConv f g a‖ ≤ l2Norm f * l2Norm g

$L^\infty$ form of the convolution bound: ‖f *_M g‖_{L^∞} ≤ ‖f‖₂ · ‖g‖₂. This is Lemma 2 from BKT's Subsection 7.3 (Multiplicative Convolution and Projections).