OAI/Geometry/EinsteinFour/ScalarPoissonKernelMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual Riemannian volume has full support. This follows directly from the local Lipschitz chart comparison, without an assumed density formula.

  1. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_open_pos line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_isOpenPosMeasure line 56
  3. theorem OAI.PositiveEinsteinFour.Geometry.normalizedVolume_isOpenPosMeasure line 60