OAI/Geometry/Arnold/Coordinates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.CriticalBound.matrixAction line 17

    Source documentation

    The actual real-matrix action on C5, jointly continuous bilinear.

    def matrixAction : RM →L[ℝ] CV →L[ℝ] CV :=
…

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CV

  2. lemma OAI.ArnoldCounterexample.CriticalBound.matrixAction_apply line 23
  3. def OAI.ArnoldCounterexample.CriticalBound.rotationDerivative line 26

    Source documentation

    Intrinsic derivative along the genuine coordinate-plane rotation.

    def rotationDerivative (G : CV → ℝ) (a b : Fin 5) (z : CV) : ℝ :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  4. lemma OAI.ArnoldCounterexample.CriticalBound.rotationDerivative_contDiff line 29
  5. def OAI.ArnoldCounterexample.CriticalBound.negativeRotationMatrix line 34

    Source documentation

    Smooth negative gradient written in the spanning infinitesimal rotations.

    def negativeRotationMatrix (G : CV → ℝ) (z : CV) : RM :=
…

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.CriticalBound.RM

  6. def OAI.ArnoldCounterexample.CriticalBound.gradientSquare line 37
  7. lemma OAI.ArnoldCounterexample.CriticalBound.negativeRotationMatrix_contDiff line 40
  8. lemma OAI.ArnoldCounterexample.CriticalBound.gradientSquare_contDiff line 45
  9. lemma OAI.ArnoldCounterexample.CriticalBound.gradientSquare_nonneg line 50
  10. lemma OAI.ArnoldCounterexample.CriticalBound.gradientSquare_eq_zero_iff line 53
  11. lemma OAI.ArnoldCounterexample.CriticalBound.negativeRotationMatrix_skew line 60
  12. lemma OAI.ArnoldCounterexample.CriticalBound.negativeRotationMatrix_derivative line 65
  13. def OAI.ArnoldCounterexample.CriticalBound.gradientCurve line 73

    Source documentation

    Orthogonal exponential is a globally defined smooth deformation of K.

    def gradientCurve (G : CV → ℝ) (p : ℝ × CV) : CV :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  14. lemma OAI.ArnoldCounterexample.CriticalBound.matrix_exp_contDiff line 76
  15. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_contDiff line 79
  16. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_preserves line 85
  17. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_zero line 89
  18. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_derivative_zero line 93
  19. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_lyapunov_derivative line 101
  20. lemma OAI.ArnoldCounterexample.CriticalBound.matrix_orbit_derivative_zero line 118
  21. lemma OAI.ArnoldCounterexample.CriticalBound.rotationDerivative_phase line 126
  22. lemma OAI.ArnoldCounterexample.CriticalBound.negativeRotationMatrix_phase line 145
  23. lemma OAI.ArnoldCounterexample.CriticalBound.gradientSquare_phase line 151
  24. lemma OAI.ArnoldCounterexample.CriticalBound.gradientCurve_phase line 157
  25. def OAI.ArnoldCounterexample.CriticalBound.tangentMatrix line 170

    Source documentation

    A literal real skew matrix lifting any horizontal vector.

    def tangentMatrix (z v : CV) : RM := fun i j ↦ 2 * (v i * star (z j) - z i * star (v j)).re

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.CriticalBound.RM

  26. lemma OAI.ArnoldCounterexample.CriticalBound.tangentMatrix_skew line 172
  27. lemma OAI.ArnoldCounterexample.CriticalBound.complex_tangentMatrix line 177
  28. lemma OAI.ArnoldCounterexample.CriticalBound.tangentMatrix_act line 183
  29. lemma OAI.ArnoldCounterexample.CriticalBound.skew_rotation_sum line 209
  30. lemma OAI.ArnoldCounterexample.CriticalBound.horizontal_derivative_of_rotation_zero line 223

    Source documentation

    Vanishing of the finitely many rotation derivatives really implies vanishing in every horizontal tangent direction.

    lemma horizontal_derivative_of_rotation_zero (G : CV → ℝ) (z : UnitQuadric)
    (hzero : ∀ a b, rotationDerivative G a b z = 0)
    (v : CV) (hv : Horizontal z v) : fderiv ℝ G z v = 0 := by
…

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.CriticalBound.rotationDerivative, OAI.ArnoldCounterexample.Horizontal