OAI/Geometry/RCD/Metric/SignedWeightedRadon.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radon–Nikodym densities of weighted full signed sources

  1. theorem OAI.RegularPointCoordinates.signed_rnDeriv_toSignedMeasure line 18
  2. theorem OAI.RegularPointCoordinates.signed_rnDeriv_bounded_density line 32
  3. theorem OAI.RegularPointCoordinates.signed_rnDeriv_sourceWeight line 63