OAI/Probability/SKValue/Control/ControlStability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.controlAccum_L1_bound line 14
2. lemma OAI.SKValue.controlAccum_memLp_of_interval line 26
3. lemma OAI.SKValue.controlAccum_sub line 36
4. lemma OAI.SKValue.controlAccum_difference_bound line 47
5. def OAI.SKValue.elapsedPayoff line 57
6. lemma OAI.SKValue.elapsedPayoff_integrable line 61
7. lemma OAI.SKValue.elapsedPayoff_difference_bound line 73