OAI/Geometry/SmoothYau/Limits/CompactFullProfileMargin.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.ProfileForm line 18
  2. def OAI.YauCounterexamples.profileTrace line 20
  3. def OAI.YauCounterexamples.profileStrict line 22
  4. def OAI.YauCounterexamples.profileFull line 25
  5. lemma OAI.YauCounterexamples.continuous_profileTrace line 29
  6. theorem OAI.YauCounterexamples.profileStrict_eventually line 39
  7. theorem OAI.YauCounterexamples.isOpen_profileFull line 72
  8. theorem OAI.YauCounterexamples.compact_positive_linear_penalty line 99
  9. def OAI.YauCounterexamples.profileRankOne line 143
  10. lemma OAI.YauCounterexamples.profileRankOne_apply line 146
  11. lemma OAI.YauCounterexamples.profileTrace_add_rankOne line 150
  12. lemma OAI.YauCounterexamples.profileStrict_rankOne line 159
  13. theorem OAI.YauCounterexamples.isOpen_profileStrict_nonzero line 167
  14. theorem OAI.YauCounterexamples.compact_strict_profile_stability line 175
  15. theorem OAI.YauCounterexamples.compact_full_profile_stability line 189
  16. theorem OAI.YauCounterexamples.preparation_rankOne_full line 203
  17. theorem OAI.YauCounterexamples.compact_full_profile_margin line 251
  18. lemma OAI.YauCounterexamples.profileForm_diag_sub_bound line 282
  19. theorem OAI.YauCounterexamples.exists_transverse_unit_near line 296
  20. lemma OAI.YauCounterexamples.profileTrace_abs_bound line 349
  21. lemma OAI.YauCounterexamples.profileTrace_sub_bound line 371
  22. theorem OAI.YauCounterexamples.profileTrace_base_lower line 413
  23. theorem OAI.YauCounterexamples.compact_profileTrace_base_lower line 460