OAI/Geometry/Arnold/Symplectic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArnoldCounterexample.Forms.CSpace line 14
  2. def OAI.ArnoldCounterexample.Forms.reCoord line 16
  3. def OAI.ArnoldCounterexample.Forms.imCoord line 19
  4. lemma OAI.ArnoldCounterexample.Forms.reCoord_apply line 22
  5. lemma OAI.ArnoldCounterexample.Forms.imCoord_apply line 23
  6. def OAI.ArnoldCounterexample.Forms.symplectic line 26

    Source documentation

    Exactly the normalization d(sum x dy-y dx).

    def symplectic (n : ℕ) : CSpace n →L[ℝ] CSpace n →L[ℝ] ℝ :=
…

    Mentions: OAI.ArnoldCounterexample.Forms.CSpace

  7. lemma OAI.ArnoldCounterexample.Forms.symplectic_apply line 30
  8. lemma OAI.ArnoldCounterexample.Forms.symplectic_skew line 34
  9. lemma OAI.ArnoldCounterexample.Forms.symplectic_eq line 42
  10. def OAI.ArnoldCounterexample.Forms.normSq line 47

    Source documentation

    Euclidean squared norm, not the sup norm of the Pi ambient Banach space.

    def normSq (n : ℕ) (z : CSpace n) : ℝ := ∑ i, Complex.normSq (z i)

    Mentions: OAI.ArnoldCounterexample.Forms.CSpace

  11. lemma OAI.ArnoldCounterexample.Forms.normSq_contDiff line 49
  12. lemma OAI.ArnoldCounterexample.Forms.normSq_nonneg line 57
  13. lemma OAI.ArnoldCounterexample.Forms.normSq_eq_zero_iff line 60
  14. lemma OAI.ArnoldCounterexample.Forms.normSq_smul line 69
  15. lemma OAI.ArnoldCounterexample.Forms.symplectic_I_left line 73
  16. lemma OAI.ArnoldCounterexample.Forms.normSq_fderiv line 87

    Source documentation

    The radial derivative identity making the curvature basic on unit spheres.

    lemma normSq_fderiv (n : ℕ) (z v : CSpace n) :
    fderiv ℝ (normSq n) z v = -symplectic n (Complex.I • z) v := by
…

    Mentions: OAI.ArnoldCounterexample.Forms.CSpace, OAI.ArnoldCounterexample.Forms.normSq, OAI.ArnoldCounterexample.Forms.symplectic