ChartVolumeDensity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The local metric volume density and its exact coordinate change law. Identification with the metric Hausdorff measure is a separate step.

theorem OAI.PositiveEinsteinFour.Geometry.sqrt_det_congruence line 17
def OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity line 26
theorem OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity_pos line 29
theorem OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity_contDiffAt line 33
theorem OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity_transition line 46
Source documentation
The density transforms by the absolute determinant of the actual derivative of the chart transition.
```
theorem chartVolumeDensity_transition (g : SmoothMetric M) (c d : M) (z : FourSpace)
    (hz : z ∈ (chartAt FourSpace c).target)
    (hx : (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source) :
    chartVolumeDensity g c z = |(chartTransitionMatrix c d z).det| *
      chartVolumeDensity g d (chartTransition c d z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransition
theorem OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity_mul_frame_det line 57
Source documentation
In orthonormal frame coordinates the metric density cancels the absolute determinant of the frame matrix.
```
theorem chartVolumeDensity_mul_frame_det (g : SmoothMetric M) (c : M) (z : FourSpace)
    (hz : z ∈ (chartAt FourSpace c).target) (E : Mat4)
    (hE : Eᵀ * metricInChart g c z * E = 1) :
    chartVolumeDensity g c z * |E.det| = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity