noncomputable def LargeSieveMultConv.l2NormSq {N : ℕ} (f : Fin N → ℂ) : ℝ

Squared $L^2$ norm of a function f : Fin N → ℂ: $\sum_n |f(n)|^2$.

noncomputable def LargeSieveMultConv.highFreqProjMulConvLinf (N₁ N₂ p : ℕ) (hp : Nat.Prime p) (f : Fin N₁ → ℂ) (g : Fin N₂ → ℂ) : ℝ

The $L^\infty(\mathbb{Z}_p^*)$ norm of the high-frequency part of the multiplicative convolution (π_p f *_M π_p g)_H^* over the unit group of ZMod p.

noncomputable def LargeSieveMultConv.largeSieveMultConvLHS (N₁ N₂ M : ℕ) (f : Fin N₁ → ℂ) (g : Fin N₂ → ℂ) : ℝ

Left-hand side of the large-sieve / multiplicative convolution theorem: ∑_{p ∈ P_M} ‖(π_p(f *_M g))_h^*‖_{L^∞}^2.

noncomputable def LargeSieveMultConv.l2Norm {N : ℕ} (f : Fin N → ℂ) : ℝ

$L^2$ norm of f : Fin N → ℂ: the square root of l2NormSq f.

theorem largeSieveMultConvLHS_le_combined (N₁ N₂ M : ℕ) (hM : 0 < M) (f : Fin N₁ → ℂ) (g : Fin N₂ → ℂ) : LargeSieveMultConv.largeSieveMultConvLHS N₁ N₂ M f g ≤ ((↑N₁ / ↑M + ↑M) * (↑N₂ / ↑M + ↑M)) ^ (1 / 2) * LargeSieveMultConv.l2Norm f * LargeSieveMultConv.l2Norm g

Combined bound used as a black box for the main theorem: the LHS is at most $((N_1/M + M)(N_2/M + M))^{1/2} \cdot \|f\|_{L^2} \cdot \|g\|_{L^2}$ (without an extra constant).

theorem LargeSieveMultConv.large_sieve_mult_conv : ∃ C > 0, ∀ (N₁ N₂ M : ℕ), 0 < M → ∀ (f : Fin N₁ → ℂ) (g : Fin N₂ → ℂ), largeSieveMultConvLHS N₁ N₂ M f g ≤ C * ((↑N₁ / ↑M + ↑M) * (↑N₂ / ↑M + ↑M)) ^ (1 / 2) * l2Norm f * l2Norm g

Large sieve and multiplicative convolution theorem: if f : [N₁] → ℂ and g : [N₂] → ℂ, then f *_M g : [N₁ N₂] → ℂ, and $$\sum_{p \in P_M} \|(\pi_p(f *_M g))_h^*\|_{L^\infty}^2 \lesssim \big((N_1/M + M)(N_2/M + M)\big)^{1/2} \|f\|_{L^2} \|g\|_{L^2}.$$