Public statement.

def AVenhance.IsAdmissibleStream (φ : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Admissible stream functions of the construction (source 1398-1414, 1457-1461): C^∞ in (t,x) and ℤ × ℤ²-periodic (φ (t + n) (x + k) = φ t x). The normalization ⟨φ_m⟩ = 0 of e.phim.bm is deliberately not part of admissibility (see proposal).

Equations

• AVenhance.IsAdmissibleStream φ = (ContDiff ℝ (↑⊤) (Function.uncurry φ) ∧ ∀ (n : ℤ) (k : Fin 2 → ℤ) (t : ℝ) (x : Homogenization.Vec 2), φ (t + ↑n) (x + AVenhance.latticeShift k) = φ t x)