Pointwise finite support of the summed corrector in its mode index.

def AVenhance.Infra.Section3.ChiMSupport.xiMKIndexWindow {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : Set ℤ

Bounded window of integer indices that can support the time cutoff.

Equations

• AVenhance.Infra.Section3.ChiMSupport.xiMKIndexWindow I m t = {k : ℤ | ↑k ∈ Set.Icc (t / AVenhance.tau β I.Λ m - 5 / 4) (t / AVenhance.tau β I.Λ m + 5 / 4)}

theorem AVenhance.Infra.Section3.ChiMSupport.xiMKIndexWindow_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (t : ℝ) : (xiMKIndexWindow I m t).Finite

theorem AVenhance.Infra.Section3.xiMK_index_mem_window {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hxi : I.xiMK m k t ≠ 0) : k ∈ ChiMSupport.xiMKIndexWindow I m t

A nonzero xiMK index must lie in a real interval of length 5/2.

theorem AVenhance.Infra.Section3.xiMK_support_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : {k : ℤ | I.xiMK m k t ≠ 0}.Finite

At a fixed time, only finitely many terms occur in the chiM sum.