Algebraic consequences of the global flow characterization.

theorem AVenhance.Infra.Flow.flow_eq_of_isFlow (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {X Y : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hY : IsFlow b Y) : X = Y

The global Lipschitz hypothesis makes an integral curve unique from one value.

theorem AVenhance.Infra.Flow.flow_group_law (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s r t : ℝ) : X t (X r x s) r = X t x s

Flow maps compose according to their time parameters.

theorem AVenhance.Infra.Flow.flow_lattice_equivariant (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) (hPeriodic : ∀ (t : ℝ), IsZ2Periodic (b t)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) (k : Fin 2 → ℤ) : X t (x + latticeShift k) s = X t x s + latticeShift k

Spatial lattice equivariance of a flow for a lattice-periodic vector field.

theorem AVenhance.Infra.Flow.flow_time_shift_one (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) (hPeriodic : ∀ (t : ℝ) (x : Homogenization.Vec 2), b (t + 1) x = b t x) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : X (t + 1) x (s + 1) = X t x s

Shifting both time arguments by one preserves a flow of a one-periodic field.

theorem AVenhance.Infra.Flow.flow_continuous_time (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s : ℝ) : Continuous fun (t : ℝ) => X t x s

Every time slice of a global flow is continuous in the target time.