Classical regularity and incompressibility of the admissible stream velocity.

theorem AVenhance.Infra.Classical.streamVel_smoothPeriodic (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) : Flow.SmoothPeriodicField (streamVel φ)

The velocity generated by an admissible stream is smooth and jointly periodic.

theorem AVenhance.Infra.Classical.streamVel_global_derivative_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : ℝ × Homogenization.Vec 2), ‖iteratedFDeriv ℝ n (Function.uncurry (streamVel φ)) p‖ ≤ C

Every fixed-order space-time derivative of the admissible stream velocity is globally bounded. The bound depends on the derivative order.

theorem AVenhance.Infra.Classical.Drift.streamVel_mixed_partials_cancel (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y 0) x 1 = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y 1) x 0

theorem AVenhance.Infra.Classical.streamVel_vecDiv_eq_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) : vecDiv (streamVel φ t) x = 0

Every spatial slice of an admissible stream velocity has zero classical divergence.