OAI/Geometry/CAT0Fillings/Bubble/Moments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.RadialSobolev.sobolevP line 13
2. def OAI.CAT0Fillings.RadialSobolev.sobolevQ line 14
3. def OAI.CAT0Fillings.RadialSobolev.bubble line 15
4. def OAI.CAT0Fillings.RadialSobolev.bubbleMass line 16
5. lemma OAI.CAT0Fillings.RadialSobolev.sobolev_exponents line 19
6. lemma OAI.CAT0Fillings.RadialSobolev.bubble_pos line 28
7. lemma OAI.CAT0Fillings.RadialSobolev.bubble_continuous line 31
8. lemma OAI.CAT0Fillings.RadialSobolev.bubble_power_p line 37
9. lemma OAI.CAT0Fillings.RadialSobolev.bubble_power_q line 45
10. lemma OAI.CAT0Fillings.RadialSobolev.bubbleMoment_algebra line 54
11. lemma OAI.CAT0Fillings.RadialSobolev.bubble_moments_integrable line 69
12. lemma OAI.CAT0Fillings.RadialSobolev.bubble_mass_pos line 82
13. lemma OAI.CAT0Fillings.RadialSobolev.bubble_moments line 87