Deformation Volume

theorem EulerDeformationVolume.determinant_hasDerivAt (F M : ℝ → Matrix (Fin 3) (Fin 3) ℝ) (t : ℝ) (hF : ∀ (i j : Fin 3), HasDerivAt (fun (s : ℝ) => F s i j) ((M t * F t) i j) t) : HasDerivAt (fun (s : ℝ) => (F s).det) ((M t).trace * (F t).det) t

Jacobi's formula along the three-dimensional deformation equation, including singular matrices; no inverse determinant is used.

theorem EulerDeformationVolume.determinant_eq_one (F M : ℝ → Matrix (Fin 3) (Fin 3) ℝ) (a b : ℝ) (hF : ∀ t ∈ Set.Icc a b, ∀ (i j : Fin 3), HasDerivAt (fun (s : ℝ) => F s i j) ((M t * F t) i j) t) (htrace : ∀ t ∈ Set.Ico a b, (M t).trace = 0) (hinit : (F a).det = 1) (t : ℝ) : t ∈ Set.Icc a b → (F t).det = 1

A trace-free velocity gradient preserves the actual deformation determinant.

theorem EulerDeformationVolume.measurePreserving_of_det_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → E) (F : E → E →L[ℝ] E) (hf : ∀ (x : E), HasFDerivAt f (F x) x) (hbij : Function.Bijective f) (hdet : ∀ (x : E), (F x).det = 1) : MeasureTheory.MeasurePreserving f μ μ

A bijective differentiable map with unit Jacobian preserves Lebesgue measure.