OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootDisintegration.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Disintegration in the actual upper-root charts

Both the final Gaussian transversal and the finite product of root times are standard Borel spaces. The open quotient charts therefore give finite coordinate measures and genuine conditional probability kernels.

  1. lemma OAI.DukePrimeDegree.isClosed_zeroPattern line 20
  2. lemma OAI.DukePrimeDegree.isOpen_nonzeroPivots line 30
  3. instance OAI.DukePrimeDegree.specialLinear_standardBorel line 38
  4. instance OAI.DukePrimeDegree.eliminationSlice_standardBorel line 46
  5. instance OAI.DukePrimeDegree.EliminationChain.time_secondCountable line 51
  6. instance OAI.DukePrimeDegree.EliminationChain.time_polish line 60
  7. instance OAI.DukePrimeDegree.EliminationChain.time_measurableSpace line 69
  8. instance OAI.DukePrimeDegree.EliminationChain.time_borelSpace line 73
  9. instance OAI.DukePrimeDegree.EliminationChain.time_standardBorel line 77
  10. instance OAI.DukePrimeDegree.EliminationChain.time_nonempty line 81
  11. abbrev OAI.DukePrimeDegree.UpperRootBox.domain line 88
  12. abbrev OAI.DukePrimeDegree.UpperRootBox.param line 89
  13. def OAI.DukePrimeDegree.UpperRootBox.range line 90
  14. lemma OAI.DukePrimeDegree.UpperRootBox.range_open line 92
  15. def OAI.DukePrimeDegree.UpperRootBox.coordinateMeasure line 94
  16. instance OAI.DukePrimeDegree.UpperRootBox.coordinateMeasure_finite line 98
  17. lemma OAI.DukePrimeDegree.UpperRootBox.map_coordinateMeasure line 107
  18. def OAI.DukePrimeDegree.UpperRootBox.conditionalKernel line 114
  19. instance OAI.DukePrimeDegree.UpperRootBox.conditionalKernel_markov line 117
  20. theorem OAI.DukePrimeDegree.UpperRootBox.disintegrate line 122