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

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

ζ_{m,k}, e.zeta.mk.def (1246).

Equations

• I.zetaMK m k = AVenhance.scaledCutoff I.zeta (AVenhance.tau β I.Λ m) k