Lebesgue measure is preserved by divergence-free smooth flows.

theorem AVenhance.Infra.Flow.flow_measurePreserving_of_divergence_free {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), spatialDivergence b t x = 0) (s t : ℝ) : MeasureTheory.MeasurePreserving (fun (x : Homogenization.Vec 2) => X t x s) MeasureTheory.volume MeasureTheory.volume

A divergence-free smooth periodic vector field generates a measure-preserving spatial flow map at every pair of times.