OAI/Geometry/EinsteinFour/EuclideanHausdorffFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean four-dimensional Hausdorff measure is a fixed positive multiple of Lebesgue measure. Its numerical normalization is immaterial for the normalized canonical frame measure.

  1. def OAI.PositiveEinsteinFour.Geometry.euclideanHausdorffFactor line 23
  2. theorem OAI.PositiveEinsteinFour.Geometry.euclideanHausdorffFactor_pos line 26
  3. theorem OAI.PositiveEinsteinFour.Geometry.euclideanHausdorff_eq_smul_volume line 29
  4. theorem OAI.PositiveEinsteinFour.Geometry.euclideanHausdorff_apply line 33