Local finite-sum continuity of the time-dependent corrector.

theorem AVenhance.Infra.Section3.xiMK_index_abs_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (t₀ t : ℝ) (k : ℤ) (ht : t ∈ Set.Icc (t₀ - 1) (t₀ + 1)) (hxi : I.xiMK m k t ≠ 0) : |↑k| ≤ (|t₀| + 1) / tau β I.Λ m + 5 / 4

theorem AVenhance.Infra.Section3.ChiMTimeRegularity.chiM_eq_bounded_index_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (κ t₀ t : ℝ) (x : Homogenization.Vec 2) (N : ℕ) (hN : (|t₀| + 1) / tau β I.Λ m + 2 < ↑N) (ht : t ∈ Set.Icc (t₀ - 1) (t₀ + 1)) : I.chiM κ m t x = ∑ k ∈ Finset.Icc (-↑N) ↑N, I.xiMK m k t • I.chiMK κ m k t x