OAI/Geometry/CAT0Fillings/Transport/Sharp.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.RadialSobolev.bubble_intervals_tendsto line 14
2. lemma OAI.CAT0Fillings.RadialSobolev.sobolev_power_complement line 27
3. lemma OAI.CAT0Fillings.RadialSobolev.bubble_normalization_energy line 34
4. theorem OAI.CAT0Fillings.RadialSobolev.radial_sharp line 43
5. lemma OAI.CAT0Fillings.RadialSobolev.omega_pos line 83
6. lemma OAI.CAT0Fillings.RadialSobolev.sphere_rpow_bubble line 88
7. lemma OAI.CAT0Fillings.RadialSobolev.polar_sharp_coefficient line 102
8. theorem OAI.CAT0Fillings.RadialSobolev.radial_sharp_polar line 125