OAI/Geometry/CAT0Fillings/Radial/ClosedInequality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CAT0Fillings.radial_inequality_of_extremal line 21
2. def OAI.CAT0Fillings.ChartGeometry.radialA line 104
3. def OAI.CAT0Fillings.ChartGeometry.radialB line 106
4. lemma OAI.CAT0Fillings.ChartGeometry.radius_bound line 109
5. lemma OAI.CAT0Fillings.ChartGeometry.memLp_radialA line 112
6. lemma OAI.CAT0Fillings.ChartGeometry.memLp_radialB line 132
7. def OAI.CAT0Fillings.ChartGeometry.radialDefect line 142
8. lemma OAI.CAT0Fillings.ChartGeometry.continuous_radialDefect line 146
9. lemma OAI.CAT0Fillings.ChartGeometry.radialDefect_eq_integral line 151