OAI/Geometry/EinsteinFour/WeylEstimates06.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Averaging the lower polar integral over the actual frame probability.

  1. def OAI.PositiveEinsteinFour.Geometry.actualBallRadialMass line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.measurable_actualBallRadialMass line 21
  3. theorem OAI.PositiveEinsteinFour.Geometry.actualBallRadialMass_subtype line 27
  4. theorem OAI.PositiveEinsteinFour.Geometry.exponential_ball_integral_radial_mass line 49
  5. theorem OAI.PositiveEinsteinFour.Geometry.lower_canonical_radial_mass_le_volume line 61