Joint first-order regularity of the actual spatial flow Jacobian.

noncomputable def AVenhance.Infra.Section4.amnrFlowJacobianEntry (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (i j : Fin 2) (z : ℝ × Homogenization.Vec 2) : ℝ

An actual spatial Jacobian entry with a fixed initial time.

Equations

• AVenhance.Infra.Section4.amnrFlowJacobianEntry X s i j z = (fderiv ℝ (fun (y : Homogenization.Vec 2) => X z.1 y s) z.2) (Homogenization.basisVec i) j

theorem AVenhance.Infra.Section4.amnrFlowJacobianEntry_spatial_fderiv_apply {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (x v : Homogenization.Vec 2) (i j : Fin 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => amnrFlowJacobianEntry X s i j (t, y)) x) v = amnrFlowSecondEval X s v (Homogenization.basisVec i) (t, x) j

The spatial derivative of a Jacobian entry is an evaluation of the actual second derivative, in the source row convention.

theorem AVenhance.Infra.Section4.amnrFlowJacobianEntry_spatial_fderiv_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) (i j : Fin 2) : Continuous fun (z : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => amnrFlowJacobianEntry X s i j (z.1, y)) z.2

The derivative with respect to the initial point is jointly continuous in target time and initial point.

theorem AVenhance.Infra.Section4.amnrFlowJacobianEntry_hasDerivAt_time {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) : HasDerivAt (fun (r : ℝ) => amnrFlowJacobianEntry X s i j (r, x)) ((Flow.jointSpatialFDeriv b t (X t x s)) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) (Homogenization.basisVec i)) j) t

The Jacobian follows the actual linearized flow equation, at all times.

theorem AVenhance.Infra.Section4.amnrFlowJacobianEntry_time_derivative_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) (i j : Fin 2) : Continuous fun (z : ℝ × Homogenization.Vec 2) => (Flow.jointSpatialFDeriv b z.1 (X z.1 z.2 s)) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X z.1 y s) z.2) (Homogenization.basisVec i)) j

The linearized equation's right side is jointly continuous.

theorem AVenhance.Infra.Section4.amnrFlowJacobianEntry_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) (i j : Fin 2) : ContDiff ℝ 1 (amnrFlowJacobianEntry X s i j)

Combining the actual time and spatial derivatives gives joint C¹ regularity of every flow-Jacobian entry, including at the initial time.