OAI/NumberTheory/DukePrimeDegree/Entropy/FutureFiberKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The local future conditional as a self-consistent Markov kernel

  1. def OAI.DukePrimeDegree.futureSliceKernel line 19
  2. def OAI.DukePrimeDegree.normalizedFutureSliceKernel line 36
  3. def OAI.DukePrimeDegree.futureFiberTimeKernel line 47
  4. lemma OAI.DukePrimeDegree.futureFiberTimeKernel_apply_good line 57
  5. lemma OAI.DukePrimeDegree.futureFiberTimeKernel_apply_zero line 73
  6. instance OAI.DukePrimeDegree.futureFiberTimeKernel_markov line 84
  7. def OAI.DukePrimeDegree.futureFiberCoordinateKernel line 97
  8. instance OAI.DukePrimeDegree.futureFiberCoordinateKernel_markov line 102
  9. lemma OAI.DukePrimeDegree.futureFiberCoordinateKernel_apply line 109
  10. theorem OAI.DukePrimeDegree.futureFiberCoordinateKernel_self_constant line 117
  11. theorem OAI.DukePrimeDegree.futureFiberCoordinateKernel_stationary line 155
  12. theorem OAI.DukePrimeDegree.futureFiberCoordinateKernel_stationary_restrict line 170