OAI/NumberTheory/DukePrimeDegree/Geometry/RowRootBox.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual row-root boxes in the lattice quotient

The simultaneous row chart descends through the discrete lattice covering. Its local product boxes cover every point and disintegrate the restricted ambient measure along the entire row group.

  1. def OAI.DukePrimeDegree.rowQuotientParametrization line 20
  2. lemma OAI.DukePrimeDegree.rowQuotientParametrization_localHomeomorph line 24
  3. lemma OAI.DukePrimeDegree.rowQuotientParametrization_add line 30
  4. structure OAI.DukePrimeDegree.RowRootBox line 38
  5. abbrev OAI.DukePrimeDegree.RowRootBox.domain line 49
  6. abbrev OAI.DukePrimeDegree.RowRootBox.param line 50
  7. def OAI.DukePrimeDegree.RowRootBox.range line 51
  8. lemma OAI.DukePrimeDegree.RowRootBox.range_open line 53
  9. def OAI.DukePrimeDegree.RowRootBox.coordinateMeasure line 55
  10. instance OAI.DukePrimeDegree.RowRootBox.coordinateMeasure_finite line 59
  11. lemma OAI.DukePrimeDegree.RowRootBox.map_coordinateMeasure line 68
  12. def OAI.DukePrimeDegree.RowRootBox.conditionalKernel line 76
  13. instance OAI.DukePrimeDegree.RowRootBox.conditionalKernel_markov line 79
  14. theorem OAI.DukePrimeDegree.RowRootBox.disintegrate line 84
  15. theorem OAI.DukePrimeDegree.exists_rowRootBox_at_coordinates line 92
  16. theorem OAI.DukePrimeDegree.exists_rowRootBox_at line 101