OAI/Geometry/Arnold/Field.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Field.symplectic line 16

    Source documentation

    The ambient symplectic bilinear form, with the factor 2 normalization.

    def symplectic : CV →L[ℝ] CV →L[ℝ] ℝ :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  2. lemma OAI.ArnoldCounterexample.Field.symplectic_apply line 19
  3. lemma OAI.ArnoldCounterexample.Field.symplectic_skew line 28
  4. def OAI.ArnoldCounterexample.Field.rotor line 38
  5. lemma OAI.ArnoldCounterexample.Field.rotor_apply line 42
  6. lemma OAI.ArnoldCounterexample.Field.rotor_phase line 44
  7. lemma OAI.ArnoldCounterexample.Field.bilinear_rotor line 48
  8. lemma OAI.ArnoldCounterexample.Field.moment_hasFDerivAt line 52
  9. def OAI.ArnoldCounterexample.Field.leftOperator line 66
  10. def OAI.ArnoldCounterexample.Field.rightOperator line 69
  11. lemma OAI.ArnoldCounterexample.Field.left_hasFDerivAt line 72
  12. lemma OAI.ArnoldCounterexample.Field.right_hasFDerivAt line 79
  13. lemma OAI.ArnoldCounterexample.Field.left_phase line 86
  14. lemma OAI.ArnoldCounterexample.Field.right_phase line 90
  15. def OAI.ArnoldCounterexample.Field.SkewAt line 95

    Source documentation

    A real-skew field is simultaneously tangent to every sphere and complex quadric.

    def SkewAt (z v : CV) : Prop := (bilinear (star z) v).re = 0 ∧ bilinear z v = 0

    Mentions: OAI.ArnoldCounterexample.CV

  16. lemma OAI.ArnoldCounterexample.Field.skewAt_zero line 97
  17. lemma OAI.ArnoldCounterexample.Field.skewAt_add line 98
  18. lemma OAI.ArnoldCounterexample.Field.skewAt_sub line 100
  19. lemma OAI.ArnoldCounterexample.Field.skewAt_smul line 103
  20. lemma OAI.ArnoldCounterexample.Field.skewAt_sum line 109
  21. lemma OAI.ArnoldCounterexample.Field.rotor_skew line 118
  22. lemma OAI.ArnoldCounterexample.Field.left_skew line 123
  23. lemma OAI.ArnoldCounterexample.Field.right_skew line 129
  24. lemma OAI.ArnoldCounterexample.Field.exists_radial line 142
  25. def OAI.ArnoldCounterexample.Field.radial line 153
  26. lemma OAI.ArnoldCounterexample.Field.radial_smooth line 154
  27. lemma OAI.ArnoldCounterexample.Field.radial_eq line 155
  28. lemma OAI.ArnoldCounterexample.Field.radial_eventually line 158
  29. lemma OAI.ArnoldCounterexample.Field.radial_squared line 163
  30. lemma OAI.ArnoldCounterexample.Field.radial_at_one line 176
  31. def OAI.ArnoldCounterexample.Field.casimir line 179
  32. def OAI.ArnoldCounterexample.Field.pairing line 181
  33. def OAI.ArnoldCounterexample.Field.mixedField line 183
  34. def OAI.ArnoldCounterexample.Field.selfField line 186
  35. def OAI.ArnoldCounterexample.Field.potential line 189

    Source documentation

    A degree-two Hamiltonian near the unit fixed quadric, with restriction f.

    def potential (z : CV) : ℝ := leftSphere z 0 - rightSphere z 2 + radial (casimir z) * pairing z

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.Field.radial, OAI.ArnoldCounterexample.Field.casimir, OAI.ArnoldCounterexample.Field.pairing

  36. def OAI.ArnoldCounterexample.Field.core line 191
  37. lemma OAI.ArnoldCounterexample.Field.casimir_smooth line 194
  38. lemma OAI.ArnoldCounterexample.Field.pairing_smooth line 199
  39. lemma OAI.ArnoldCounterexample.Field.potential_smooth line 206
  40. lemma OAI.ArnoldCounterexample.Field.mixed_smooth line 213
  41. lemma OAI.ArnoldCounterexample.Field.self_smooth line 219
  42. lemma OAI.ArnoldCounterexample.Field.core_smooth line 224
  43. lemma OAI.ArnoldCounterexample.Field.casimir_hasFDerivAt line 230
  44. lemma OAI.ArnoldCounterexample.Field.pairing_hasFDerivAt line 242
  45. lemma OAI.ArnoldCounterexample.Field.core_hamiltonian line 253
  46. lemma OAI.ArnoldCounterexample.Field.core_skew line 264