OAI/NumberTheory/DukePrimeDegree/Geometry/MatrixCoordinateFrames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coordinate frames on the actual velocity-rank events

The finite-dimensional recurrence argument uses rectangular matrices with one natural-number row dimension. Flattening the actual matrix space is only a linear change of coordinates. On each measurable rank event the selected velocity frame has independent columns and spans the actual velocity space; outside that event the rectangular frame is zero.

  1. def OAI.DukePrimeDegree.matrixCoordinateEquiv line 24
  2. def OAI.DukePrimeDegree.coordinateVelocityFrame line 40
  3. lemma OAI.DukePrimeDegree.coordinateVelocityFrame_eq line 45
  4. lemma OAI.DukePrimeDegree.coordinateVelocityFrame_eq_zero line 53
  5. theorem OAI.DukePrimeDegree.coordinateVelocityFrame_linearIndependent line 58
  6. theorem OAI.DukePrimeDegree.coordinateVelocityFrame_span line 69
  7. theorem OAI.DukePrimeDegree.measurable_coordinateVelocityFrame_entry line 82
  8. def OAI.DukePrimeDegree.matrixCoordinateWeight line 101
  9. lemma OAI.DukePrimeDegree.matrixCoordinateWeight_pos line 104
  10. lemma OAI.DukePrimeDegree.matrixCoordinateEquiv_diagonal_conjugation line 107