C² regularity of the Jacobian and C³ regularity of the flow on forward strips.

theorem AVenhance.Infra.Flow.JointC3Forward.jointSpatialFDeriv_contDiff_all {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => jointSpatialFDeriv b p.1 p.2

noncomputable def AVenhance.Infra.Flow.JointC3Forward.flowSpatialJacobianFixedStart (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (p : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Spatial Jacobian of the flow with the starting time fixed.

Equations

• AVenhance.Infra.Flow.JointC3Forward.flowSpatialJacobianFixedStart X s p = fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y s) p.2

noncomputable def AVenhance.Infra.Flow.JointC3Forward.flowSpatialJacobianTimeDerivative (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (p : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Observation-time derivative of the spatial Jacobian, given by the variational equation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Flow.JointC3Forward.flowSpatialJacobianFullDerivative (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Full time-space differential of the spatial Jacobian with starting time fixed.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_contDiffOn_two_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) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y s) p.2) (Set.Ioo s T ×ˢ Set.univ)

The spatial Jacobian is C² in target time and initial position on forward open strips, with the start time fixed.