OAI/GroupTheory/PolycyclicRecognition/Analysis/LeftInvariantRiemannianMetric.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A left-invariant Riemannian metric

An inner product at the identity is transported by the actual differentials of left translation. Its smoothness is checked in the tangent bundle charts.

  1. def OAI.PolycyclicRecognition.leftInvariantInner line 23
  2. theorem OAI.PolycyclicRecognition.leftInvariantInner_pos line 27
  3. theorem OAI.PolycyclicRecognition.leftInvariantInner_bounded line 32
  4. def OAI.PolycyclicRecognition.leftLogCoordinate line 36
  5. theorem OAI.PolycyclicRecognition.contMDiffAt_leftLogCoordinate line 40
  6. theorem OAI.PolycyclicRecognition.leftInvariantInner_coordinates line 56
  7. theorem OAI.PolycyclicRecognition.contMDiff_leftInvariantInner line 69
  8. def OAI.PolycyclicRecognition.leftInvariantRiemannianMetric line 82
  9. theorem OAI.PolycyclicRecognition.leftInvariantInner_mul line 90