Second-order Taylor control for smooth periodic vector fields.

theorem AVenhance.Infra.Flow.exists_global_spatialSecondFDeriv_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖iteratedFDeriv ℝ 2 (fun (y : Homogenization.Vec 2) => b t y) x‖ ≤ C

A fixed-time spatial slice of a smooth periodic field has a globally bounded second derivative, with a bound independent of the chosen time.

theorem AVenhance.Infra.Flow.exists_global_spatialThirdFDeriv_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖iteratedFDeriv ℝ 3 (fun (y : Homogenization.Vec 2) => b t y) x‖ ≤ C

A fixed-time spatial slice of a smooth periodic field has a globally bounded third derivative, with a bound independent of the chosen time.

theorem AVenhance.Infra.Flow.exists_global_spatialFDeriv_apply_taylor_remainder {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x y v : Homogenization.Vec 2), ‖(jointSpatialFDeriv b t y) v - (jointSpatialFDeriv b t x) v - (fderiv ℝ (fun (z : Homogenization.Vec 2) => (jointSpatialFDeriv b t z) v) x) (y - x)‖ ≤ C * ‖v‖ * ‖y - x‖ * ‖y - x‖

After fixing the direction acted on by the Jacobian, its first-order Taylor remainder is quadratic, uniformly in time and base point.

theorem AVenhance.Infra.Flow.exists_global_smoothPeriodicField_taylor_remainder {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t y - b t x - (fderiv ℝ (fun (z : Homogenization.Vec 2) => b t z) x) (y - x)‖ ≤ C * ‖y - x‖ * ‖y - x‖

A globally quadratic remainder estimate for the first-order Taylor approximation of a smooth periodic vector field in space.

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

The spatial derivative of a smooth periodic field is globally Lipschitz in space, uniformly in time.