OAI/NumberTheory/DukePrimeDegree/Geometry/TransverseDiagonalData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Diagonal coordinates on the transverse lower triangular slice

Column ratios are fixed by the diagonal action; the logarithms of the absolute diagonal entries are translated linearly. These are the actual transverse coordinates, before choosing any finite entropy approximation.

  1. lemma OAI.DukePrimeDegree.upperRootTransverse_lowerTriangular line 18
  2. lemma OAI.DukePrimeDegree.upperRootTransverse_diagonal_ne_zero line 25
  3. def OAI.DukePrimeDegree.transverseColumnRatios line 33
  4. def OAI.DukePrimeDegree.transverseLogDiagonal line 36
  5. lemma OAI.DukePrimeDegree.continuous_transverseColumnRatios line 39
  6. lemma OAI.DukePrimeDegree.continuous_transverseLogDiagonal line 49
  7. lemma OAI.DukePrimeDegree.transverseColumnRatios_diagonal line 57
  8. lemma OAI.DukePrimeDegree.transverseLogDiagonal_diagonal line 67
  9. lemma OAI.DukePrimeDegree.transverse_data_injective line 78