OAI/Geometry/RCD/Coordinates/NormalizedDensityLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact probability laws from nonnegative densities

The normalizing integral is retained explicitly, including for measurable pullbacks to the original metric space.

  1. def OAI.RegularPointCoordinates.normalizedDensityLaw line 18
  2. theorem OAI.RegularPointCoordinates.normalizedDensityLaw_integral line 25
  3. theorem OAI.RegularPointCoordinates.normalizedDensityLaw_le line 36
  4. theorem OAI.RegularPointCoordinates.normalizedDensityLaw_tendsto line 47