OAI/NumberTheory/DukePrimeDegree/Dynamics/KernelVelocityFrames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual measurable frames for component stabilizers

Projecting the Euclidean coordinate basis and selecting a maximal Gram minor constructs a frame of each actual stabilizer velocity space. The frame cardinality and every fixed column are measurable along a Markov kernel. This supplies the missing measurable input to diagonal recurrence.

  1. def OAI.DukePrimeDegree.euclideanVelocityColumns line 21
  2. theorem OAI.DukePrimeDegree.euclideanVelocityColumns_span line 26
  3. theorem OAI.DukePrimeDegree.measurable_euclideanVelocityColumns line 40
  4. def OAI.DukePrimeDegree.velocityFrameCard line 60
  5. def OAI.DukePrimeDegree.velocityFrame line 63
  6. theorem OAI.DukePrimeDegree.velocityFrame_linearIndependent line 67
  7. theorem OAI.DukePrimeDegree.velocityFrame_span line 73
  8. theorem OAI.DukePrimeDegree.velocityFrameCard_eq_finrank line 94
  9. theorem OAI.DukePrimeDegree.measurable_velocityFrameCard line 100
  10. theorem OAI.DukePrimeDegree.measurable_velocityFrame line 107