Statement file: zetaProd (Section3). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.Ingredients.zetaProd {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (s : ℝ) : ℝ

The coefficient ζ̂_{m,l_k}(s) ζ_{m,k}(s) in e.parabcorr.k, e.Chimk.formula, e.psi.m.

Equations

• I.zetaProd m k s = I.hatZetaML m (AVenhance.lIdx β I.Λ m k) s * I.zetaMK m k s