OAI/Geometry/RCD/Metric/FiniteSignedRadon.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radon–Nikodym derivatives of finite signed coordinate sums

  1. lemma OAI.RegularPointCoordinates.signed_rnDeriv_zero line 17
  2. lemma OAI.RegularPointCoordinates.signed_rnDeriv_sum line 22
  3. lemma OAI.RegularPointCoordinates.signed_rnDeriv_sum_smul line 33