RiemannianVolume.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The measure in the geometric application is fixed by the metric. In four Euclidean dimensions the diameter-normalized Hausdorff measure is multiplied by the unit-ball factor (pi^2 / 2) / 2^4. Positivity and finiteness are kept separate from the elementary probability normalization.

def OAI.PositiveEinsteinFour.Geometry.volumeMeasure line 23
Source documentation
Canonically normalized four-dimensional Riemannian volume, constructed from the actual length metric rather than an unspecified measure.
```
def volumeMeasure (g : SmoothMetric M) : Measure M := by
…
```
def OAI.PositiveEinsteinFour.Geometry.totalVolume line 30
def OAI.PositiveEinsteinFour.Geometry.volumeRatio line 33
Source documentation
The volume ratio with the curvature-one round four-sphere.
```
def volumeRatio (g : SmoothMetric M) : ℝ := totalVolume g / (8 * Real.pi ^ 2 / 3)
```
Mentions: OAI.PositiveEinsteinFour.Geometry.totalVolume
def OAI.PositiveEinsteinFour.Geometry.normalizedVolume line 35
structure OAI.PositiveEinsteinFour.Geometry.FinitePositiveVolume line 40
Source documentation
Compact Riemannian volume has positive finite mass. The normalization argument below only needs these two facts, and does not assume a volume bound.
```
structure FinitePositiveVolume (g : SmoothMetric M) : Prop where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.normalizedVolume_isProbability line 44
theorem OAI.PositiveEinsteinFour.Geometry.totalVolume_pos line 51
theorem OAI.PositiveEinsteinFour.Geometry.volumeRatio_pos line 55