OAI/Geometry/CAT0Fillings/Sobolev/Compact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.closed_sobolev_bound line 19
2. theorem OAI.CAT0Fillings.extremal_closed_sobolev line 84
3. lemma OAI.CAT0Fillings.ChartGeometry.norm_valueProjection_le line 119
4. lemma OAI.CAT0Fillings.ChartGeometry.norm_gradientProjection_le line 122
5. lemma OAI.CAT0Fillings.ChartGeometry.totallyBounded_inclusion line 126
6. theorem OAI.CAT0Fillings.ChartGeometry.inclusion_compact line 180