OAI/Geometry/CAT0Fillings/Sobolev/Constant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ChartGeometry.lipSobolev line 18
2. lemma OAI.CAT0Fillings.ChartGeometry.inclusion_lipSobolev line 21
3. lemma OAI.CAT0Fillings.ChartGeometry.closedGradient_lipSobolev line 23
4. lemma OAI.CAT0Fillings.ChartGeometry.gradient_const line 26
5. def OAI.CAT0Fillings.ChartGeometry.constant line 34
6. lemma OAI.CAT0Fillings.ChartGeometry.closedGradient_constant line 36
7. lemma OAI.CAT0Fillings.ChartGeometry.criticalNorm_constant line 39
8. lemma OAI.CAT0Fillings.ChartGeometry.norm_inclusion_constant_sq line 50
9. instance OAI.CAT0Fillings.ChartGeometry.sobolev_separable line 56