OAI/Geometry/EinsteinFour/GeodesicGeometry06.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Canceling the radial cubic measure against the actual exponential Jacobian leaves the determinant of the normal Jacobi tensor itself.

  1. theorem OAI.PositiveEinsteinFour.Geometry.radial_cubic_cancel line 22
  2. theorem OAI.PositiveEinsteinFour.Geometry.minimizing_exponential_integral_radial line 29
  3. theorem OAI.PositiveEinsteinFour.Geometry.exponential_ball_integral_radial line 99
  4. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_sphericalJacobi_lintegral line 182
  5. theorem OAI.PositiveEinsteinFour.Geometry.euclidean_lintegral_polar line 235
  6. theorem OAI.PositiveEinsteinFour.Geometry.radial_weight_cancel line 258
  7. theorem OAI.PositiveEinsteinFour.Geometry.minimizing_exponential_weighted_radial line 266
  8. theorem OAI.PositiveEinsteinFour.Geometry.volume_lintegral_le_weighted_exponential line 305
  9. theorem OAI.PositiveEinsteinFour.Geometry.volume_lintegral_le_weighted_radial line 321