OAI/Geometry/PolarProducts/FiniteDescent.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLinking.conePoint line 19
  2. def OAI.SmoothLinking.degreeMap line 21
  3. theorem OAI.SmoothLinking.degreeMap_eq_self line 27
  4. theorem OAI.SmoothLinking.contDiffAt_degreeMap_pos line 39
  5. theorem OAI.SmoothLinking.contDiff_degreeMap line 56
  6. theorem OAI.SmoothLinking.norm_translate_le line 72
  7. theorem OAI.SmoothLinking.degreeMap_identity_outside line 81
  8. theorem OAI.SmoothLinking.sphere_linking line 92
  9. theorem OAI.FlowDescent.curve_displacement line 137
  10. theorem OAI.FlowDescent.curve_energy_deriv line 150
  11. theorem OAI.FlowDescent.curve_energy_antitone line 159
  12. theorem OAI.FlowDescent.step_energy_le line 169
  13. theorem OAI.FlowDescent.step_energy_drop line 176
  14. theorem OAI.FlowDescent.iterate_norm_le line 221
  15. theorem OAI.FlowDescent.iterate_energy_le line 233
  16. theorem OAI.FlowDescent.iterate_energy_drop line 242
  17. theorem OAI.FlowDescent.contDiff_iterate line 273
  18. theorem OAI.FlowDescent.exists_descent_map line 282