OAI/Analysis/NodalLength/InteriorMass.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Profiles.supMass line 327
2. lemma OAI.SharpNodal.Profiles.supMass_mono line 329
3. lemma OAI.SharpNodal.Profiles.supMass_le line 332
4. lemma OAI.SharpNodal.Profiles.extract_sup_rates line 338
5. lemma OAI.SharpNodal.Profiles.sup_open_lower line 345
6. lemma OAI.SharpNodal.Profiles.sup_compact_upper line 357
7. def OAI.SharpNodal.Profiles.SupLocalBound line 387
8. lemma OAI.SharpNodal.Profiles.supProfile_lt_local line 390
9. lemma OAI.SharpNodal.Profiles.supProfile_le_of_local line 399
10. lemma OAI.SharpNodal.Profiles.normalized_supProfile line 411
11. lemma OAI.SharpNodal.Profiles.normalized_supProfile_max line 427
12. lemma OAI.SharpNodal.Profiles.bounded_potential_L2_interior line 455
13. lemma OAI.SharpNodal.Profiles.bounded_potential_supMass line 515
14. lemma OAI.SharpNodal.Profiles.polynomial_exponential_gap line 548
15. def OAI.SharpNodal.Profiles.plainMass line 572
16. lemma OAI.SharpNodal.Profiles.plainMass_mono line 573
17. lemma OAI.SharpNodal.Profiles.plainMass_center line 574
18. lemma OAI.SharpNodal.Profiles.plainMass_tilted line 576
19. lemma OAI.SharpNodal.Profiles.plainMass_le_sup line 578
20. lemma OAI.SharpNodal.Profiles.local_sup_mass line 584