Infrastructure for the §2 construction.

theorem AVenhance.Infra.Construction.fderiv_slice {φ : ℝ → Homogenization.Vec 2 → ℝ} (h : IsAdmissibleStream φ) (t : ℝ) (x v : Homogenization.Vec 2) : (fderiv ℝ (φ t) x) v = (fderiv ℝ (Function.uncurry φ) (t, x)) (0, v)

theorem AVenhance.Infra.Construction.contDiff_partial {φ : ℝ → Homogenization.Vec 2 → ℝ} (h : IsAdmissibleStream φ) (v : Homogenization.Vec 2) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry φ) p) (0, v)

theorem AVenhance.Infra.Construction.streamVel_apply {φ : ℝ → Homogenization.Vec 2 → ℝ} (h : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) : streamVel φ t x = ![-(fderiv ℝ (Function.uncurry φ) (t, x)) (0, Homogenization.basisVec 1), (fderiv ℝ (Function.uncurry φ) (t, x)) (0, Homogenization.basisVec 0)]

theorem AVenhance.Infra.Construction.smoothPeriodic_streamVel {φ : ℝ → Homogenization.Vec 2 → ℝ} (h : IsAdmissibleStream φ) : Flow.SmoothPeriodicField (streamVel φ)

The velocity of an admissible stream is a smooth jointly periodic field.