OAI/Geometry/RCD/Sobolev/CompactRestrictedLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Probability laws on a measurable compact support

The subtype law has the exact normalized restriction as its ambient law, and an explicit bounded nonnegative density. Compactness is supplied only where the heat-factor construction uses it.

  1. theorem OAI.RegularPointCoordinates.restricted_probability_law line 18
  2. theorem OAI.RegularPointCoordinates.restricted_law_integral line 54