OAI/Analysis/LipschitzEquivalence/RotatingStages.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.RotatingStages.path line 18
  2. theorem OAI.LipschitzCounterexample.RotatingStages.path_zero line 23
  3. theorem OAI.LipschitzCounterexample.RotatingStages.path_contDiff line 26
  4. theorem OAI.LipschitzCounterexample.RotatingStages.inner_path_stage line 34
  5. theorem OAI.LipschitzCounterexample.RotatingStages.norm_path line 46
  6. theorem OAI.LipschitzCounterexample.RotatingStages.path_small_eventually line 63
  7. theorem OAI.LipschitzCounterexample.RotatingStages.path_large_eventually line 72
  8. theorem OAI.LipschitzCounterexample.RotatingStages.norm_angular line 91
  9. theorem OAI.LipschitzCounterexample.RotatingStages.rotation_deriv_bound line 100
  10. theorem OAI.LipschitzCounterexample.RotatingStages.path_derivative_budget line 139
  11. theorem OAI.LipschitzCounterexample.SlowAngles.angle_antitone line 186
  12. theorem OAI.LipschitzCounterexample.SlowAngles.theta_antitone line 208
  13. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_contDiffAt line 217