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

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

ξ_{m,k}, e.xi.mk.def (1283), defined here for all k ∈ ℤ.

Equations

• I.xiMK m k = AVenhance.scaledCutoff I.xi (AVenhance.tau β I.Λ m) k