OAI/Probability/MemoryPrecision/StochasticContinuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.stochRoute line 21
2. lemma OAI.MemoryPrecision.measurable_stochRoute line 27
3. lemma OAI.MemoryPrecision.stochRoute_sum_le_one line 37
4. def OAI.MemoryPrecision.stochCont line 53
5. lemma OAI.MemoryPrecision.measurable_stochCont line 59
6. lemma OAI.MemoryPrecision.stochCont_le_one line 71
7. lemma OAI.MemoryPrecision.stochCont_unroll line 83