OAI/Geometry/NearbyLagrangian/SphereCollapse.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Sphere cap collapses, smooth plateaus and localization of tube families.

  1. abbrev OAI.NearbyLagrangian.SphereCollapse.Sphere line 21
  2. def OAI.NearbyLagrangian.SphereCollapse.antipode line 23
  3. lemma OAI.NearbyLagrangian.SphereCollapse.norm_coe line 27
  4. lemma OAI.NearbyLagrangian.SphereCollapse.blend_ne_zero line 30
  5. def OAI.NearbyLagrangian.SphereCollapse.homotopy line 56
  6. lemma OAI.NearbyLagrangian.SphereCollapse.homotopy_zero line 73
  7. lemma OAI.NearbyLagrangian.SphereCollapse.homotopy_one_eq line 79
  8. def OAI.NearbyLagrangian.SphereCollapse.collapse line 85
  9. def OAI.NearbyLagrangian.SphereCollapse.idHomotopyCollapse line 90
  10. def OAI.NearbyLagrangian.SphereCollapse.cutoff line 107
  11. lemma OAI.NearbyLagrangian.SphereCollapse.cutoff_mem line 112
  12. lemma OAI.NearbyLagrangian.SphereCollapse.cutoff_antipode line 116
  13. def OAI.NearbyLagrangian.SphereCollapse.capCollapse line 119
  14. def OAI.NearbyLagrangian.SphereCollapse.capHomotopy line 122
  15. lemma OAI.NearbyLagrangian.SphereCollapse.capCollapse_eq line 126
  16. theorem OAI.NearbyLagrangian.SphereCollapse.localize_family line 132
  17. def OAI.NearbyLagrangian.SphereCollapse.plateauParameter line 150
  18. lemma OAI.NearbyLagrangian.SphereCollapse.plateauParameter_zero line 158
  19. lemma OAI.NearbyLagrangian.SphereCollapse.plateauParameter_one line 165
  20. theorem OAI.NearbyLagrangian.SphereCollapse.move_plateau line 173
  21. theorem OAI.NearbyLagrangian.SphereCollapse.localize_to_value line 201
  22. instance OAI.NearbyLagrangian.Tubes.tubePathConnected line 215

    Distinct definitions of this name: OAI/Geometry/NearbyLagrangian/TubeClasses.lean:122 (same statement text; different proof or body). Qualify references as OAI.NearbyLagrangian.Tubes.tubePathConnected@path.

  23. theorem OAI.NearbyLagrangian.Tubes.standard_plateau line 218
  24. def OAI.NearbyLagrangian.SphereCollapse.plateauBump line 234
  25. def OAI.NearbyLagrangian.SphereCollapse.smoothPlateau line 236
  26. lemma OAI.NearbyLagrangian.SphereCollapse.smoothPlateau_mem line 240
  27. lemma OAI.NearbyLagrangian.SphereCollapse.smoothPlateau_one line 244
  28. lemma OAI.NearbyLagrangian.SphereCollapse.smoothPlateau_zero line 252
  29. lemma OAI.NearbyLagrangian.SphereCollapse.contMDiff_smoothPlateau line 258
  30. lemma OAI.NearbyLagrangian.SphereCollapse.polar_cap_in_plateau line 264
  31. theorem OAI.NearbyLagrangian.Tubes.smooth_localized_tube line 294
  32. theorem OAI.NearbyLagrangian.Tubes.smooth_localized_kernel line 316