Public statement.
noncomputable def
AVenhance.Ingredients.nextStream
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
:
ℝ → Homogenization.Vec 2 → ℝ
e.psi.recursion (1436-1455), second form: φ_m := φ_{m-1} + Σ_{k ∈ ℤ} (term_k).
The tsum over k ∈ ℤ is not junk: for each (t,x) only finitely many k contribute
(nextStream_summable).
Equations
- I.nextStream m φ hφ t x = φ t x + ∑' (k : ℤ), I.nextStreamTerm m φ hφ t x k