OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockParabolicChart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A two-block chart with the neutral factor last

Reordering the Gauss factorization gives lower-cross × upper-cross × neutral coordinates. Right multiplication by a neutral element changes only the neutral coordinate. This is the equivariance required before applying a Haar product argument to an actual invariant measure.

  1. abbrev OAI.DukePrimeDegree.TwoBlockParabolicCoordinates line 20
  2. def OAI.DukePrimeDegree.twoBlockGaussReorderEquiv line 23
  3. lemma OAI.DukePrimeDegree.continuous_twoBlockGaussReorder line 34
  4. lemma OAI.DukePrimeDegree.continuous_twoBlockGaussReorder_symm line 46
  5. def OAI.DukePrimeDegree.twoBlockGaussReorder line 68
  6. def OAI.DukePrimeDegree.twoBlockParabolicHomeomorph line 74
  7. def OAI.DukePrimeDegree.twoBlockParabolicParam line 78
  8. theorem OAI.DukePrimeDegree.twoBlockParabolicHomeomorph_symm_val line 82
  9. theorem OAI.DukePrimeDegree.twoBlockParabolicParam_isOpenEmbedding line 90
  10. theorem OAI.DukePrimeDegree.twoBlockParabolicParam_mem_cell line 102
  11. theorem OAI.DukePrimeDegree.twoBlockParabolicParam_right_neutral line 108
  12. theorem OAI.DukePrimeDegree.twoBlockGaussCell_right_neutral line 116