OAI/Geometry/CAT0Fillings/Transport/Normalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.RadialSobolev.finite_transport_estimate line 15
2. lemma OAI.CAT0Fillings.RadialSobolev.radial_integral_smul line 73
3. lemma OAI.CAT0Fillings.RadialSobolev.radial_second_moment_smul line 84
4. lemma OAI.CAT0Fillings.RadialSobolev.radial_integral_pos line 95
5. lemma OAI.CAT0Fillings.RadialSobolev.normalization_power line 104
6. lemma OAI.CAT0Fillings.RadialSobolev.normalize_transport_estimate line 108