Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Flow.FlowIntegral

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 : ℝ) :
X t x s = x + ∫ (r : ℝ) in s..t, b r (X r x s)

A trajectory of a smooth-field global flow satisfies its integral equation on every oriented finite interval.