OAI/Geometry/EinsteinFour/CotangentVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The change-of-variables step for local cotangent maps. The determinant condition is the conclusion of the variational calculation, not an assumption of measure preservation.

  1. theorem OAI.PositiveEinsteinFour.Geometry.cotangent_map_volume_of_det_one line 19

    Source documentation

    A locally injective map with unit absolute derivative determinant preserves coordinate volume on its domain.

    theorem cotangent_map_volume_of_det_one
    (f : CotangentCoordinates → CotangentCoordinates)
    (s : Set CotangentCoordinates) (hs : MeasurableSet s)
    (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : InjOn f s)
    (hdet : ∀ x ∈ s, |(cotangentJacobian f x).det| = 1) :
    Measure.map f (volume.restrict s) = volume.restrict (f '' s) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentJacobian