OAI/NumberTheory/DukePrimeDegree/Dynamics/EuclideanVelocityProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Measurable projections onto the actual component velocity spaces

The matrix topology has a concrete Euclidean model. Orthogonal projection in that model gives a finite, measurably varying spanning family for the actual stabilizer velocity space of every probability kernel. No choice of subgroup curves or of a tangent basis is made measurably.

  1. abbrev OAI.DukePrimeDegree.MatrixEuclidean line 23
  2. def OAI.DukePrimeDegree.matrixEuclideanLinearEquiv line 25
  3. def OAI.DukePrimeDegree.matrixEuclideanEquiv line 34
  4. lemma OAI.DukePrimeDegree.matrixEuclideanEquiv_apply line 39
  5. lemma OAI.DukePrimeDegree.matrixEuclideanEquiv_symm_apply line 43
  6. def OAI.DukePrimeDegree.euclideanVelocitySpace line 47
  7. def OAI.DukePrimeDegree.componentVelocityProjection line 51
  8. theorem OAI.DukePrimeDegree.componentVelocityProjection_mem line 57
  9. theorem OAI.DukePrimeDegree.componentVelocityProjection_eq_self line 63
  10. theorem OAI.DukePrimeDegree.measurable_componentVelocityProjection_entry line 76
  11. theorem OAI.DukePrimeDegree.measurable_componentVelocityProjection line 90
  12. theorem OAI.DukePrimeDegree.componentVelocityProjection_span line 101