The actual flow of a trace-free smooth bounded velocity preserves its Jacobian determinant and Haar volume, in every finite dimension.

Jacobi's formula in every finite dimension, and determinant preservation for the actual linear evolution with trace-free coefficient.

theorem EulerLinearEvolutionDeterminant.matrixJacobi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F M : ℝ → Matrix ι ι ℝ) (S : Set ℝ) (t : ℝ) (hF : HasDerivWithinAt F (M t * F t) S t) : HasDerivWithinAt (fun (s : ℝ) => (F s).det) ((M t).trace * (F t).det) S t

theorem EulerLinearEvolutionDeterminant.operatorJacobi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (F M : ℝ → E →L[ℝ] E) (S : Set ℝ) (t : ℝ) (hF : HasDerivWithinAt F (M t ∘SL F t) S t) : HasDerivWithinAt (fun (s : ℝ) => (F s).det) ((LinearMap.trace ℝ E) ↑(M t) * (F t).det) S t

The finite-dimensional Jacobi formula does not assume invertibility.

theorem EulerLinearDuhamel.Evolution.det_forward_eq_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) (htrace : ∀ (t : ↑(Set.Icc 0 T)), (LinearMap.trace ℝ E) ↑(B t) = 0) (t : ↑(Set.Icc 0 T)) : (U.forward t).det = (U.forward ⟨0, ⋯⟩).det

theorem EulerLinearDuhamel.constructedEvolution_det_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (htrace : ∀ (t : ↑(Set.Icc 0 T)), (LinearMap.trace ℝ E) ↑(B t) = 0) (t : ↑(Set.Icc 0 T)) : ((constructedEvolution T hT B).forward t).det = 1

theorem EulerSmoothBanachFlow.jacobianEvolution_det_one {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (t : ↑(Set.Icc 0 T)) (x : E) : ((jacobianEvolution T hT A x).forward t).det = 1

theorem EulerSmoothBanachFlow.forward_det_one {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (t : ↑(Set.Icc 0 T)) (x : E) : (fderiv ℝ (fun (y : E) => (flowData T hT A).forward (↑t) y) x).det = 1

theorem EulerSmoothBanachFlow.forward_measurePreserving {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving ((flowData T hT A).forward ↑t) μ μ

theorem EulerSmoothBanachFlow.backward_measurePreserving {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving ((flowData T hT A).backward ↑t) μ μ