OAI/Geometry/RCD/Sobolev/PositiveSobolevTestMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive measures representing every continuous compact Sobolev test

  1. theorem OAI.RegularPointCoordinates.exists_positive_sobolev_test_measure line 17