OAI/Geometry/CAT0Fillings/Radial/Extension.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.integrable_radialPair line 17
2. lemma OAI.CAT0Fillings.ChartGeometry.integrable_radialVariation line 25
3. lemma OAI.CAT0Fillings.ChartGeometry.radialVariation_eq_integral line 32
4. lemma OAI.CAT0Fillings.ChartGeometry.memLp_sweptCoefficient line 52
5. lemma OAI.CAT0Fillings.ChartGeometry.integrable_sweptField line 63
6. lemma OAI.CAT0Fillings.ChartGeometry.sweptMass_eq_integral line 68
7. lemma OAI.CAT0Fillings.ChartGeometry.radialDefect_lip line 102
8. lemma OAI.CAT0Fillings.ChartGeometry.radialDefect_smul line 118
9. lemma OAI.CAT0Fillings.ChartGeometry.lipSobolev_smul line 132
10. lemma OAI.CAT0Fillings.ChartGeometry.radialDefect_nonpos_lip line 137
11. lemma OAI.CAT0Fillings.ChartGeometry.radialDefect_nonpos line 159