OAI/Probability/SKValue/Equations/Cutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.OrderParameter.cutoff line 31
2. lemma OAI.SKValue.OrderParameter.cutoff_measurable line 34
3. lemma OAI.SKValue.OrderParameter.cutoff_nonneg line 48
4. lemma OAI.SKValue.OrderParameter.cutoff_integrable line 53
5. def OAI.SKValue.limitedControl line 59
6. lemma OAI.SKValue.Admissible.limited_measurable line 62
7. lemma OAI.SKValue.limitedControl_eq line 70
8. lemma OAI.SKValue.Admissible.limited_bound line 75
9. lemma OAI.SKValue.OrderParameter.intervalIntegrable line 78
10. lemma OAI.SKValue.OrderParameter.shift_integrable line 82