OAI/Geometry/RCD/Sobolev/SignedLipschitzMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positivity and uniqueness of finite signed distributions

  1. theorem OAI.RegularPointCoordinates.signed_integral_jordan line 16
  2. theorem OAI.RegularPointCoordinates.signedMeasure_nonneg_of_lipschitz_integral line 27
  3. theorem OAI.RegularPointCoordinates.signedMeasure_eq_of_lipschitz_integral line 48