OAI/Geometry/CAT0Fillings/Compactness/Interpolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.JointBV.lintegral_enorm_rpow_eq line 15
2. lemma OAI.CAT0Fillings.JointBV.eLpNorm_two_interpolation line 21
3. lemma OAI.CAT0Fillings.JointBV.lpNorm_two_sq_interpolation line 41
4. lemma OAI.CAT0Fillings.ChartGeometry.dist_value line 73
5. lemma OAI.CAT0Fillings.ChartGeometry.totallyBounded_value_of_lpBound line 81
6. theorem OAI.CAT0Fillings.ChartGeometry.totallyBounded_value line 122