OAI/Geometry/Arnold/Midpoint.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ArnoldCounterexample.Midpoint.contraction line 17
  2. def OAI.ArnoldCounterexample.Midpoint.resolvent line 29

    Source documentation

    The inverse of id-sX, for a smooth uniformly small parameter s.

    def resolvent (X : E → E) {C : ℝ≥0} (hX : LipschitzWith C X)
    (τ : ℝ → ℝ) (hτ : ∀ t, ‖τ t‖ * C < 1) (p : ℝ × E) : E :=
…
  3. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_eq line 33
  4. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_unique line 38
  5. lemma OAI.ArnoldCounterexample.Midpoint.implicit_partial line 44
  6. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_smooth line 57
  7. lemma OAI.ArnoldCounterexample.Midpoint.neg_small line 89
  8. def OAI.ArnoldCounterexample.Midpoint.step line 93

    Source documentation

    The implicit midpoint step. The actual step size is 2τ.

    def step (X : E → E) {C : ℝ≥0} (hX : LipschitzWith C X)
    (τ : ℝ → ℝ) (hτ : ∀ t, ‖τ t‖ * C < 1) (p : ℝ × E) : E :=
…
  9. lemma OAI.ArnoldCounterexample.Midpoint.step_center line 97
  10. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_step line 107
  11. lemma OAI.ArnoldCounterexample.Midpoint.step_inverse line 116
  12. lemma OAI.ArnoldCounterexample.Midpoint.step_smooth line 123
  13. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_zero line 128
  14. lemma OAI.ArnoldCounterexample.Midpoint.step_zero line 133
  15. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_symmetry line 139
  16. lemma OAI.ArnoldCounterexample.Midpoint.step_symmetry line 150
  17. lemma OAI.ArnoldCounterexample.Midpoint.resolvent_fderiv_equation line 156
  18. lemma OAI.ArnoldCounterexample.Midpoint.hamiltonian_linearization line 181
  19. def OAI.ArnoldCounterexample.Midpoint.hamiltonian line 200
  20. lemma OAI.ArnoldCounterexample.Midpoint.hamiltonian_smooth line 204
  21. lemma OAI.ArnoldCounterexample.Midpoint.step_time_derivative line 212
  22. lemma OAI.ArnoldCounterexample.Midpoint.step_hamiltonian_equation line 223