OAI/Geometry/SmoothYau/NodalMeasure/PositiveIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.MetricIntegralAtlas.positiveIntegral line 18
2. def OAI.YauCounterexamples.MetricIntegralAtlas.volumeMeasure line 28
3. instance OAI.YauCounterexamples.MetricIntegralAtlas.volumeMeasure_finite line 30
4. lemma OAI.YauCounterexamples.MetricIntegralAtlas.mean_eq_volumeIntegral line 34
5. instance OAI.YauCounterexamples.MetricIntegralAtlas.volumeMeasure_openPos line 39