OAI/Probability/SKSupport/Foundations/Control.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.zeroControl line 16
2. theorem OAI.ZeroTemperatureSK.extend_coe line 25
3. lemma OAI.ZeroTemperatureSK.OrderParameter.extend_nonneg line 28
4. lemma OAI.ZeroTemperatureSK.OrderParameter.measurable_extend line 34
5. lemma OAI.ZeroTemperatureSK.Control.measurable line 39
6. lemma OAI.ZeroTemperatureSK.Control.measurable_elapsed line 56
7. lemma OAI.ZeroTemperatureSK.Control.integrable_weighted line 62
8. lemma OAI.ZeroTemperatureSK.Control.integrable_weighted_sq line 69