Joint first-order regularity for the §4 flow slices.

theorem AVenhance.Infra.Section5.FrozenFlowRegularity.streamFlowSmooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : Flow.SmoothPeriodicField (streamVel (Φ (m - 1)))

theorem AVenhance.Infra.Section5.FrozenFlowRegularity.streamFlowIsFlow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : IsFlow (streamVel (Φ (m - 1))) (flow (streamVel (Φ (m - 1))) ⋯ ⋯)

theorem AVenhance.Infra.Section5.xFlowInv_joint_contDiff_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ 1 fun (p : ℝ × Homogenization.Vec 2) => I.xFlowInv hΦ m l p.1 p.2

The inverse flow slice is jointly C¹ in target time and position.

theorem AVenhance.Infra.Section5.xFlowInv_hasFDerivAt {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : HasFDerivAt (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l s y) (fderiv ℝ (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l s y) (t, x)) (t, x)

The joint Fréchet derivative needed by the inverse-flow transport rule is provided by the flow definitions and the smoothness of the preceding admissible stream.

theorem AVenhance.Infra.Section5.xFlow_spatial_contDiff_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 2 (I.xFlow hΦ m l t)

Every forward flow slice is C² in the initial spatial point.

theorem AVenhance.Infra.Section5.xFlowInv_spatial_contDiff_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 2 (I.xFlowInv hΦ m l t)

Every inverse flow slice is C² in the spatial point.

theorem AVenhance.Infra.Section5.xFlow_spatial_contDiff_three {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 3 (I.xFlow hΦ m l t)

Every forward flow slice is C³ in its initial spatial point.

theorem AVenhance.Infra.Section5.xFlowInv_spatial_contDiff_three {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 3 (I.xFlowInv hΦ m l t)

Every inverse flow slice is C³ in its spatial point.