OAI/Analysis/NodalLength/Subdivision.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SharpNodal.Profiles.NormalizedPDEData line 146
2. def OAI.SharpNodal.Profiles.NormalizedPDEData.Small line 162
3. def OAI.SharpNodal.Profiles.NormalizedPDEData.HasGridCorrection line 167
4. theorem OAI.SharpNodal.Profiles.uniform_normalized_subdivision line 173
5. def OAI.SharpNodal.Profiles.centeredMass line 213
6. lemma OAI.SharpNodal.Profiles.centeredMass_mono line 216
7. lemma OAI.SharpNodal.Profiles.tiltedMass_centered line 220
8. lemma OAI.SharpNodal.Profiles.tilted_excess_centered line 241
9. lemma OAI.SharpNodal.Profiles.tilted_finite_centered line 251
10. lemma OAI.SharpNodal.Profiles.centeredMass_weight_bound line 263
11. lemma OAI.SharpNodal.Profiles.massExcess_log_sub line 284
12. lemma OAI.SharpNodal.Profiles.massExcess_weight_bound line 289
13. lemma OAI.SharpNodal.Profiles.profile_zero_on_ball line 313
14. theorem OAI.SharpNodal.Profiles.profile_strong_maximum line 338
15. lemma OAI.SharpNodal.Profiles.centeredMass_ne_zero_of line 370
16. lemma OAI.SharpNodal.Profiles.centeredMass_ne_top_of line 377
17. lemma OAI.SharpNodal.Profiles.centered_excess_nonneg line 382
18. lemma OAI.SharpNodal.Profiles.centered_excess_weight_bound line 394
19. lemma OAI.SharpNodal.Profiles.normalized_inner_rate_eq line 412
20. lemma OAI.SharpNodal.Profiles.tiltedMass_weight_mono line 433
21. lemma OAI.SharpNodal.Profiles.tiltedMass_weight_add_const line 446
22. lemma OAI.SharpNodal.Profiles.tiltedMass_zero_center line 471
23. theorem OAI.SharpNodal.Profiles.one_subdivision line 477