OAI/Geometry/RCD/Coordinates/PullbackDensityLaws.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual source probability densities with prescribed Euclidean limits

  1. theorem OAI.RegularPointCoordinates.pullback_density_integrable line 14
  2. def OAI.RegularPointCoordinates.pullbackDensityLaw line 20
  3. theorem OAI.RegularPointCoordinates.pullbackDensityLaw_integral line 26
  4. theorem OAI.RegularPointCoordinates.pullback_density_mass_tendsto line 32
  5. theorem OAI.RegularPointCoordinates.pullback_density_laws_tendsto line 42