OAI/Geometry/Arnold/CompactField.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Field.cutoff line 13
  2. def OAI.ArnoldCounterexample.Field.vectorField line 15
  3. lemma OAI.ArnoldCounterexample.Field.cutoff_eq_one line 17
  4. lemma OAI.ArnoldCounterexample.Field.vectorField_smooth line 22
  5. lemma OAI.ArnoldCounterexample.Field.norm_bound_of_normSquared line 25
  6. lemma OAI.ArnoldCounterexample.Field.vectorField_compact line 33
  7. lemma OAI.ArnoldCounterexample.Field.vectorField_lipschitz line 46
  8. lemma OAI.ArnoldCounterexample.Field.vectorField_local_core line 49
  9. lemma OAI.ArnoldCounterexample.Field.vectorField_hamiltonian line 54
  10. lemma OAI.ArnoldCounterexample.Field.vectorField_skew line 59
  11. lemma OAI.ArnoldCounterexample.Field.rotor_zero_coordinate line 61
  12. lemma OAI.ArnoldCounterexample.Field.left_zero_coordinate line 64
  13. lemma OAI.ArnoldCounterexample.Field.right_zero_coordinate line 67
  14. lemma OAI.ArnoldCounterexample.Field.core_zero_coordinate line 70
  15. lemma OAI.ArnoldCounterexample.Field.vectorField_zero_coordinate line 73
  16. lemma OAI.ArnoldCounterexample.Field.rotor_zero_rest line 76
  17. lemma OAI.ArnoldCounterexample.Field.vectorField_zero_rest line 80
  18. lemma OAI.ArnoldCounterexample.Field.vectorField_zero line 87
  19. lemma OAI.ArnoldCounterexample.Field.moment_scale line 90
  20. lemma OAI.ArnoldCounterexample.Field.left_scale line 97
  21. lemma OAI.ArnoldCounterexample.Field.right_scale line 101
  22. lemma OAI.ArnoldCounterexample.Field.casimir_phase line 105
  23. lemma OAI.ArnoldCounterexample.Field.pairing_phase line 108
  24. lemma OAI.ArnoldCounterexample.Field.core_phase line 111
  25. lemma OAI.ArnoldCounterexample.Field.vectorField_phase line 120
  26. lemma OAI.ArnoldCounterexample.Field.potential_phase line 124