OAI/Geometry/EinsteinFour/SphericalMeasureMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite positive mass of the actual Hausdorff measure on the unit three-sphere, and hence the probability normalization used by the moments.

  1. theorem OAI.PositiveEinsteinFour.Angular.threeSpace_hausdorff_haar line 15
  2. theorem OAI.PositiveEinsteinFour.Angular.faceChart_measure_lt_top line 22

    Source documentation

    Compact smooth face images have finite three-dimensional measure.

    theorem faceChart_measure_lt_top (i : Fin 4) (t : Bool) :
    (Measure.hausdorffMeasure 3 : Measure FourSpace)
      (faceChart i t '' Metric.closedBall (0 : ThreeSpace) 2) < ⊤ := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.faceChart, OAI.PositiveEinsteinFour.Angular.ThreeSpace

  3. theorem OAI.PositiveEinsteinFour.Angular.sphere_hausdorff_measure_lt_top line 33
  4. theorem OAI.PositiveEinsteinFour.Angular.sphere_hausdorff_measure_pos line 46
  5. theorem OAI.PositiveEinsteinFour.Angular.direction_hausdorff_mass_eq line 58

    Source documentation

    Hausdorff measure on the subtype agrees with the ambient measure.

    theorem direction_hausdorff_mass_eq :
    (Measure.hausdorffMeasure 3 : Measure Directions) Set.univ =
      (Measure.hausdorffMeasure 3 : Measure FourSpace) {v | ‖v‖ = 1} := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.Directions

  6. theorem OAI.PositiveEinsteinFour.Angular.direction_hausdorff_mass_pos line 69
  7. theorem OAI.PositiveEinsteinFour.Angular.direction_hausdorff_mass_lt_top line 74
  8. theorem OAI.PositiveEinsteinFour.Angular.actual_sphereMeasure_probability line 80

    Source documentation

    The concrete normalization is a genuine probability measure.

    theorem actual_sphereMeasure_probability : IsProbabilityMeasure sphereMeasure := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.sphereMeasure