OAI/Probability/SKSupport/Foundations/ControlledState.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.WeakIto.controlledState line 17
2. lemma OAI.ZeroTemperatureSK.WeakIto.controlledState_zero line 22
3. lemma OAI.ZeroTemperatureSK.WeakIto.controlledState_adapted line 26
4. lemma OAI.ZeroTemperatureSK.WeakIto.controlledState_integrable line 42
5. lemma OAI.ZeroTemperatureSK.WeakIto.stepDrift_add line 53
6. lemma OAI.ZeroTemperatureSK.WeakIto.stepCost_add line 63
7. lemma OAI.ZeroTemperatureSK.WeakIto.controlledState_increment line 74
8. def OAI.ZeroTemperatureSK.WeakIto.verificationError line 90
9. lemma OAI.ZeroTemperatureSK.WeakIto.verificationError_limit line 95
10. theorem OAI.ZeroTemperatureSK.WeakIto.constant_interval_verification_upper line 107