Statement file: IsFlow (Flow).
This file contains exactly one declaration of the formalization's public statement surface.
def
AVenhance.IsFlow
(b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2)
:
Flow of a time-dependent field b on ℝ²: X t x s solves
∂ₜ X(t,x,s) = b(t, X(t,x,s)) for all t ∈ ℝ, with X(s,x,s) = x
(source: e.flow.m.def, enhance.tex 1397-1410).
Equations
- AVenhance.IsFlow b X = ((∀ (x : Homogenization.Vec 2) (s : ℝ), X s x s = x) ∧ ∀ (x : Homogenization.Vec 2) (s t : ℝ), HasDerivAt (fun (r : ℝ) => X r x s) (b t (X t x s)) t)