OAI/Geometry/Arnold/Parameter.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Construction.constant line 15
  2. lemma OAI.ArnoldCounterexample.Construction.lipschitz line 16
  3. def OAI.ArnoldCounterexample.Construction.epsilon line 18
  4. lemma OAI.ArnoldCounterexample.Construction.epsilon_pos line 19
  5. def OAI.ArnoldCounterexample.Construction.parameter line 21
  6. lemma OAI.ArnoldCounterexample.Construction.parameter_smooth line 22
  7. lemma OAI.ArnoldCounterexample.Construction.parameter_zero line 23
  8. lemma OAI.ArnoldCounterexample.Construction.parameter_one line 24
  9. lemma OAI.ArnoldCounterexample.Construction.parameter_small line 25
  10. lemma OAI.ArnoldCounterexample.Construction.parameter_contract line 37
  11. def OAI.ArnoldCounterexample.Construction.center line 40
  12. def OAI.ArnoldCounterexample.Construction.forwardMid line 41
  13. def OAI.ArnoldCounterexample.Construction.backwardMid line 42
  14. def OAI.ArnoldCounterexample.Construction.midHamiltonian line 44
  15. lemma OAI.ArnoldCounterexample.Construction.center_smooth line 47
  16. lemma OAI.ArnoldCounterexample.Construction.forwardMid_smooth line 49
  17. lemma OAI.ArnoldCounterexample.Construction.backwardMid_smooth line 51
  18. lemma OAI.ArnoldCounterexample.Construction.midHamiltonian_smooth line 53
  19. lemma OAI.ArnoldCounterexample.Construction.forwardMid_preserves line 56
  20. lemma OAI.ArnoldCounterexample.Construction.backwardMid_preserves line 58
  21. lemma OAI.ArnoldCounterexample.Construction.center_phase_general line 61
  22. lemma OAI.ArnoldCounterexample.Construction.center_phase line 68
  23. lemma OAI.ArnoldCounterexample.Construction.forwardMid_phase line 71
  24. lemma OAI.ArnoldCounterexample.Construction.backwardMid_phase line 74
  25. lemma OAI.ArnoldCounterexample.Construction.midHamiltonian_phase line 77
  26. lemma OAI.ArnoldCounterexample.Construction.backward_forward line 81
  27. lemma OAI.ArnoldCounterexample.Construction.forward_backward line 83
  28. lemma OAI.ArnoldCounterexample.Construction.forwardMid_start line 86
  29. lemma OAI.ArnoldCounterexample.Construction.center_bound line 89
  30. lemma OAI.ArnoldCounterexample.Construction.mid_equation line 93
  31. lemma OAI.ArnoldCounterexample.Construction.center_identity line 100
  32. lemma OAI.ArnoldCounterexample.Construction.forwardMid_center line 102
  33. lemma OAI.ArnoldCounterexample.Construction.center_average line 104
  34. lemma OAI.ArnoldCounterexample.Construction.center_zero_coordinate line 108
  35. lemma OAI.ArnoldCounterexample.Construction.forwardMid_zero_coordinate line 111