OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralTransverseCoordinates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The actual neutral coordinate in the upper-root chart

On the positive-diagonal chart the transverse slice is the product of its unit-diagonal part and the trace-zero logarithmic diagonal. Right diagonal translation fixes the first coordinate and translates the second. This is the local center coordinate needed for comparison with the root kernel.

  1. abbrev OAI.DukePrimeDegree.transverseNeutralSpace line 19
  2. abbrev OAI.DukePrimeDegree.PositiveTransverse line 34
  3. abbrev OAI.DukePrimeDegree.UnitDiagonalTransverse line 37
  4. lemma OAI.DukePrimeDegree.transverseLogDiagonal_sum line 40
  5. def OAI.DukePrimeDegree.transverseNeutralCoordinate line 46
  6. def OAI.DukePrimeDegree.normalizedTransverse line 50
  7. lemma OAI.DukePrimeDegree.normalizedTransverse_entry line 54
  8. lemma OAI.DukePrimeDegree.normalizedTransverse_diagonal line 62
  9. def OAI.DukePrimeDegree.transverseUnitCoordinate line 67
  10. def OAI.DukePrimeDegree.transverseNeutralReconstruct line 71
  11. lemma OAI.DukePrimeDegree.transverseNeutralReconstruct_coordinates line 79
  12. lemma OAI.DukePrimeDegree.transverseNeutralCoordinate_reconstruct line 88
  13. lemma OAI.DukePrimeDegree.transverseUnitCoordinate_reconstruct line 97
  14. lemma OAI.DukePrimeDegree.continuous_transverseNeutralCoordinate line 112
  15. lemma OAI.DukePrimeDegree.continuous_transverseUnitCoordinate line 116
  16. lemma OAI.DukePrimeDegree.continuous_transverseNeutralReconstruct line 129
  17. def OAI.DukePrimeDegree.neutralTransverseHomeomorph line 152
  18. def OAI.DukePrimeDegree.positiveTransverseDiagonal line 163
  19. lemma OAI.DukePrimeDegree.transverseNeutralCoordinate_diagonal line 171
  20. lemma OAI.DukePrimeDegree.transverseUnitCoordinate_diagonal line 177