OAI/Geometry/CAT0Fillings/Minimizers/SpatialVariation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.nonnegative_mem_closed line 20
2. lemma OAI.CAT0Fillings.ChartGeometry.nonnegative_linear_inequality line 46
3. def OAI.CAT0Fillings.ChartGeometry.spatialMass line 68
4. def OAI.CAT0Fillings.ChartGeometry.radialVariationChart line 72
5. def OAI.CAT0Fillings.ChartGeometry.radialVariation line 79
6. lemma OAI.CAT0Fillings.ChartGeometry.spatialMass_zero line 81
7. lemma OAI.CAT0Fillings.ChartGeometry.spatialMass_nonneg line 88
8. lemma OAI.CAT0Fillings.ChartGeometry.spatialMass_first_variation line 93
9. lemma OAI.CAT0Fillings.ChartGeometry.spatial_push_mass_le line 106