OAI/Probability/SKValue/Control/ControlIntegral.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.controlIntegral line 27
2. lemma OAI.SKValue.controlIntegral_eq line 31
3. lemma OAI.SKValue.controlIntegral_measurable line 43
4. lemma OAI.SKValue.controlIntegral_integrand_bound line 52
5. lemma OAI.SKValue.controlIntegral_bound line 58
6. lemma OAI.SKValue.controlIntegral_integrable line 69
7. lemma OAI.SKValue.controlIntegral_nonneg_even line 75
8. lemma OAI.SKValue.controlIntegrand_intervalIntegrable line 87
9. lemma OAI.SKValue.control_cost_bound line 98