OAI/Probability/SKSupport/Regularity/AbsExtend.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.OrderParameter.abs_extend line 14
2. lemma OAI.ZeroTemperatureSK.Control.measurable_drift_integral line 17
3. lemma OAI.ZeroTemperatureSK.Control.measurable_cost_integral line 24
4. lemma OAI.ZeroTemperatureSK.Control.drift_integral_bound line 31
5. lemma OAI.ZeroTemperatureSK.Control.cost_integral_bound line 41
6. lemma OAI.ZeroTemperatureSK.controlPayoff_measurable line 52
7. lemma OAI.ZeroTemperatureSK.controlPayoff_abs_bound line 60
8. lemma OAI.ZeroTemperatureSK.controlPayoff_integrable line 76
9. lemma OAI.ZeroTemperatureSK.controlPayoff_le line 86