Consequences of compact-cell derivative bounds for smooth periodic fields.

theorem AVenhance.Infra.Flow.exists_global_spatial_lipschitz {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (L : ℝ), 0 ≤ L ∧ ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖

The spatial slices of a smooth jointly periodic field have a common global Lipschitz constant.

theorem AVenhance.Infra.Flow.existsUnique_smoothPeriodic_flow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃! X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow b X

A smooth jointly periodic field satisfies the hypotheses of the global flow characterization.

theorem AVenhance.Infra.Flow.flow_continuous_joint_of_smoothPeriodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => X p.1 p.2.1 p.2.2

The flow is jointly continuous in target time, initial position, and initial time for every characterized flow of a smooth periodic field.

theorem AVenhance.Infra.Flow.flow_target_time_derivative_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => b p.1 (X p.1 p.2.1 p.2.2)

The right-hand side of the target-time ODE is jointly continuous in all flow parameters.