Joint continuity of the actual second flow derivative, with a fixed start. This is the regularity needed to admit the primitive material flow jet.

noncomputable def AVenhance.Infra.Section4.amnrFlowSecondEval (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (h k : Homogenization.Vec 2) (z : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

Evaluation of the actual second spatial flow derivative.

Equations

• AVenhance.Infra.Section4.amnrFlowSecondEval X s h k z = ((fderiv ℝ (fun (y : Homogenization.Vec 2) => fderiv ℝ (fun (w : Homogenization.Vec 2) => X z.1 w s) y) z.2) h) k

theorem AVenhance.Infra.Section4.amnrFlowSecondEval_continuousOn_forward {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k : Homogenization.Vec 2) (s T : ℝ) (hsT : s ≤ T) : ContinuousOn (amnrFlowSecondEval X s h k) (Set.Icc s T ×ˢ Set.univ)

The characterized second variation is the actual second flow derivative throughout every forward time interval.

theorem AVenhance.Infra.Section4.amnrFlowSecondEval_reverse (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (h k : Homogenization.Vec 2) (z : ℝ × Homogenization.Vec 2) : amnrFlowSecondEval X s h k z = amnrFlowSecondEval (Flow.regularityReverseTimeFlow X) (-s) h k (-z.1, z.2)

Reversing target and start times does not change a spatial derivative.

theorem AVenhance.Infra.Section4.amnrFlowSecondEval_continuousOn_backward {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k : Homogenization.Vec 2) (S s : ℝ) (hSs : S ≤ s) : ContinuousOn (amnrFlowSecondEval X s h k) (Set.Icc S s ×ˢ Set.univ)

Joint continuity on backward intervals follows from the same proved forward variation theorem applied to the reversed characterized flow.

theorem AVenhance.Infra.Section4.amnrFlowSecondEval_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) (h k : Homogenization.Vec 2) : Continuous (amnrFlowSecondEval X s h k)

The actual second spatial flow derivative is jointly continuous on all target times, including the diagonal at the fixed start time.