OAI/Geometry/RCD/Metric/MeasuredBallSetIntegrals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Set integrals under the exact normalized approximation laws

  1. theorem OAI.RegularPointCoordinates.normalizedBallPushforward_measurable_integral line 12
  2. theorem OAI.RegularPointCoordinates.normalizedBallPushforward_setIntegral line 32
  3. theorem OAI.RegularPointCoordinates.euclideanBallProbability_setIntegral line 49