OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootDiagonalCharts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The diagonal action on actual full upper-root quotient boxes

  1. def OAI.DukePrimeDegree.upperRootTransverseDiagonal line 14
  2. lemma OAI.DukePrimeDegree.upperRootTransverseDiagonal_add line 24
  3. lemma OAI.DukePrimeDegree.upperRootTransverseDiagonal_zero line 32
  4. def OAI.DukePrimeDegree.upperRootTransverseDiagonalHomeomorph line 38
  5. abbrev OAI.DukePrimeDegree.upperRootDiagonalCoordinates line 49
  6. lemma OAI.DukePrimeDegree.upperRootDiagonalCoordinates_param line 56
  7. def OAI.DukePrimeDegree.UpperRootBox.diagonal line 73
  8. lemma OAI.DukePrimeDegree.UpperRootBox.diagonal_domain line 96
  9. theorem OAI.DukePrimeDegree.UpperRootBox.diagonal_coordinateMeasure line 101
  10. theorem OAI.DukePrimeDegree.UpperRootBox.diagonal_conditionalKernel line 127
  11. lemma OAI.DukePrimeDegree.UpperRootBox.diagonal_marginal line 138