OAI/Probability/SKValue/Control/Controls.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.controlAccum line 11
2. lemma OAI.SKValue.progressive_clamped_measurable line 15
3. lemma OAI.SKValue.controlAccum_measurable line 26
4. lemma OAI.SKValue.controlAccum_bound line 46
5. lemma OAI.SKValue.controlAccum_integrable line 58
6. lemma OAI.SKValue.controlAccum_integrand_intervalIntegrable line 69
7. def OAI.SKValue.controlState line 96
8. lemma OAI.SKValue.controlState_past_measurable line 100
9. lemma OAI.SKValue.controlState_memLp_two line 109
10. lemma OAI.SKValue.controlState_initial line 122