Public statement.

theorem AVenhance.Ingredients.nextStream_summable {β : ℝ} (I : Ingredients β) (m : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) : Summable fun (k : ℤ) => I.nextStreamTerm m φ hφ t x k

Well-definedness of the series in e.psi.recursion: for every (t,x) the family of terms is summable (indeed finitely supported, since supp ζ_{m,k} ⊆ [(k-2/3)τ_m,(k+2/3)τ_m]).