Public statement.

def AVenhance.IsStreamSeq {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Source-characterized sequence {φ_m} of e.phi0def (1423-1433) and e.psi.recursion: φ_0 = 0 and φ_m = nextStream m φ_{m-1} (with φ_{m-1} admissible) for m ≥ 1.

Equations

• AVenhance.IsStreamSeq I Φ = ((Φ 0 = fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) ∧ ∀ (m : ℕ), 1 ≤ m → ∃ (h : AVenhance.IsAdmissibleStream (Φ (m - 1))), Φ m = I.nextStream m (Φ (m - 1)) h)