Continuity of the spatial derivative of a smooth periodic flow.

theorem AVenhance.Infra.Flow.SpatialRegularity.gronwallBound_zero_scale_regular (L a c d : ℝ) : gronwallBound 0 L (c * a) d = c * gronwallBound 0 L a d

theorem AVenhance.Infra.Flow.exists_flow_spatialFDeriv_lipschitz_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (hst : s ≤ t) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x y : Homogenization.Vec 2), ∃ (Jx : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (Jy : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), HasFDerivAt (fun (z : Homogenization.Vec 2) => X t z s) Jx x ∧ HasFDerivAt (fun (z : Homogenization.Vec 2) => X t z s) Jy y ∧ ‖Jx - Jy‖ ≤ K * ‖x - y‖

The variational derivative depends Lipschitz continuously on the base point over a forward time interval.

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_continuous_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (hst : s ≤ t) : Continuous fun (x : Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x

The spatial derivative of a forward flow map is continuous in the initial position.

def AVenhance.Infra.Flow.regularityReverseTimeField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Reverse-time vector field used in the spatial regularity argument.

Equations

• AVenhance.Infra.Flow.regularityReverseTimeField b t x = -b (-t) x

def AVenhance.Infra.Flow.regularityReverseTimeFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

Reverse-time flow used in the spatial regularity argument.

Equations

• AVenhance.Infra.Flow.regularityReverseTimeFlow X t x s = X (-t) x (-s)

theorem AVenhance.Infra.Flow.smoothPeriodicField_regularityReverseTime {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : SmoothPeriodicField (regularityReverseTimeField b)

theorem AVenhance.Infra.Flow.isFlow_regularityReverseTime {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlow (regularityReverseTimeField b) (regularityReverseTimeFlow X)

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

The spatial derivative of a characterized smooth flow is continuous in the initial position for arbitrary target and initial times.

theorem AVenhance.Infra.Flow.flow_spatial_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) : ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => X t x s

For fixed times, the spatial flow map is continuously differentiable, and its derivative is the variational flow.