Divergence under the actual determinant-one pushforward. Jacobi's formula controls the derivative of the Jacobian, and symmetry of the second derivative supplies the Piola cancellation.

@[instance_reducible]

noncomputable def EulerPacketVolumeDivergence.instPacketVolumeDivergence1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketVolumeDivergence.instPacketVolumeDivergence1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketVolumeDivergence.instPacketVolumeDivergence2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketVolumeDivergence.instPacketVolumeDivergence2 = inferInstance

theorem EulerPacketVolumeDivergence.coordinateTrace_eq_matrix (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.coordinateTrace A = Matrix.trace (EulerPacketPiola.operatorMatrix A)

theorem EulerPacketVolumeDivergence.operatorMatrix_det (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : Matrix.det (EulerPacketPiola.operatorMatrix A) = A.det

theorem EulerPacketVolumeDivergence.coordinateTrace_comp_comm (A B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.coordinateTrace (A ∘SL B) = EulerSmoothLimit.coordinateTrace (B ∘SL A)

theorem EulerPacketVolumeDivergence.coordinateTrace_conjugate (A : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.coordinateTrace ((↑A ∘SL B) ∘SL ↑A.symm) = EulerSmoothLimit.coordinateTrace B

theorem EulerPacketVolumeDivergence.determinant_derivative_trace_zero (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x v : EulerSmoothLimit.Space) (A : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hA : F x = ↑A) (hF : DifferentiableAt ℝ F x) (hdet : (fun (y : EulerSmoothLimit.Space) => Matrix.det (EulerPacketPiola.operatorMatrix (F y))) =ᶠ[nhds x] fun (x : EulerSmoothLimit.Space) => 1) : EulerSmoothLimit.coordinateTrace ((fderiv ℝ F x) v ∘SL ↑A.symm) = 0

A constant unit determinant forces the true logarithmic derivative of the frame to have zero trace in every direction.

theorem EulerPacketVolumeDivergence.divergence_of_pullback (X v w : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (A : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hX : ContDiffAt ℝ 2 X x) (hA : fderiv ℝ X x = ↑A) (hdet : (fun (y : EulerSmoothLimit.Space) => Matrix.det (EulerPacketPiola.operatorMatrix (fderiv ℝ X y))) =ᶠ[nhds x] fun (x : EulerSmoothLimit.Space) => 1) (hv : DifferentiableAt ℝ v x) (hw : DifferentiableAt ℝ w (X x)) (hpull : w ∘ X =ᶠ[nhds x] fun (y : EulerSmoothLimit.Space) => (fderiv ℝ X y) (v y)) : EulerSmoothLimit.divergence w (X x) = EulerSmoothLimit.divergence v x

The divergence of a genuine volume-preserving pushforward equals the label-space divergence. Only local C² regularity and local determinant one are needed at the point.

theorem EulerPacketVolumeDivergence.divergence_pushforward (X Y v : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (A : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hX : ContDiffAt ℝ 2 X x) (hA : fderiv ℝ X x = ↑A) (hdet : (fun (y : EulerSmoothLimit.Space) => Matrix.det (EulerPacketPiola.operatorMatrix (fderiv ℝ X y))) =ᶠ[nhds x] fun (x : EulerSmoothLimit.Space) => 1) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) (hY : DifferentiableAt ℝ Y (X x)) (hv : DifferentiableAt ℝ v x) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ X (Y y)) (v (Y y))) (X x) = EulerSmoothLimit.divergence v x