Integral formulation of a characterized flow trajectory.
theorem
AVenhance.Infra.Flow.flow_eq_initial_add_intervalIntegral
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
(x : Homogenization.Vec 2)
(s t : ℝ)
:
A trajectory of a smooth-field global flow satisfies its integral equation on every oriented finite interval.