OAI/Geometry/RCD/Metric/SignedRadonLocal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Localizing Radon–Nikodym identities of full signed measures

  1. theorem OAI.RegularPointCoordinates.signed_rnDeriv_restrict line 14
  2. theorem OAI.RegularPointCoordinates.signed_rnDeriv_eq_on_of_restrict_eq line 35
  3. theorem OAI.RegularPointCoordinates.signed_rnDeriv_density line 45