OAI/Probability/GaussianReplacement/CompletedModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentProjection.StreamKernel.CompletedLearner line 18
  2. instance OAI.CurrentProjection.StreamKernel.runStatus_singletons line 27
  3. def OAI.CurrentProjection.StreamKernel.CompletedLearner.startStatus line 53
  4. def OAI.CurrentProjection.StreamKernel.CompletedLearner.choiceStatus line 56
  5. def OAI.CurrentProjection.StreamKernel.CompletedLearner.nextLaw line 60
  6. def OAI.CurrentProjection.StreamKernel.CompletedLearner.runLaw line 69
  7. def OAI.CurrentProjection.StreamKernel.CompletedLearner.terminalStatus line 74
  8. def OAI.CurrentProjection.StreamKernel.CompletedLearner.estimateLaw line 79
  9. def OAI.CurrentProjection.StreamKernel.CompletedLearner.uniformSuccess line 85
  10. def OAI.CurrentProjection.StreamKernel.CompletedLearner.borel line 92
  11. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.borel_transition_ae line 102
  12. def OAI.CurrentProjection.StreamKernel.CompletedLearner.transitionKernel line 107
  13. instance OAI.CurrentProjection.StreamKernel.CompletedLearner.transitionKernel_markov line 113
  14. def OAI.CurrentProjection.StreamKernel.CompletedLearner.outputKernel line 116
  15. instance OAI.CurrentProjection.StreamKernel.CompletedLearner.outputKernel_markov line 118