The first spatial jet of a smooth flow is itself a characterized flow on the product of position and two direction columns.

noncomputable def AVenhance.Infra.Flow.firstJetField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2) → Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)

The augmented vector field for position and a pair of spatial directions.

Equations

• AVenhance.Infra.Flow.firstJetField b t z = (b t z.1, fun (i : Fin 2) => (AVenhance.Infra.Flow.jointSpatialFDeriv b t z.1) (z.2 i))

theorem AVenhance.Infra.Flow.firstJetField_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ContDiff ℝ (↑⊤) (Function.uncurry (firstJetField b))

The first-jet vector field is smooth on its full product state space.

noncomputable def AVenhance.Infra.Flow.firstJetFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2) → ℝ → Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)

The augmented flow: its direction columns are the spatial derivative of the original flow applied to the supplied initial columns.

Equations

• AVenhance.Infra.Flow.firstJetFlow X t z s = (X t z.1 s, fun (i : Fin 2) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) z.1) (z.2 i))

theorem AVenhance.Infra.Flow.firstJetFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlowOn (firstJetField b) (firstJetFlow X)

The position and first spatial jet satisfy their augmented ODE exactly.

theorem AVenhance.Infra.Flow.firstJetFlow_group_law {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (z : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) (s r t : ℝ) : firstJetFlow X t (firstJetFlow X r z s) r = firstJetFlow X t z s

The augmented first-jet maps obey the same composition law as the underlying flow.

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

For each pair of times, the augmented first-jet map is continuously differentiable in its initial position and direction columns.