OAI/Probability/SKSupport/Control/GridBridge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.remainingLengths line 15
2. lemma OAI.ZeroTemperatureSK.remainingLengths_shift line 18
3. lemma OAI.ZeroTemperatureSK.remainingLengths_nonpos line 25
4. lemma OAI.ZeroTemperatureSK.remainingLengths_head line 34
5. lemma OAI.ZeroTemperatureSK.remainingLengths_time line 39
6. lemma OAI.ZeroTemperatureSK.cascadeV_shift line 59
7. lemma OAI.ZeroTemperatureSK.cascadeV_uniform line 67
8. lemma OAI.ZeroTemperatureSK.finiteValue_eq_remaining line 73
9. def OAI.ZeroTemperatureSK.gridError line 124
10. lemma OAI.ZeroTemperatureSK.grid_integral_error line 127
11. lemma OAI.ZeroTemperatureSK.Control.elapsed_integral line 156
12. lemma OAI.ZeroTemperatureSK.profit_eq_integral line 164
13. lemma OAI.ZeroTemperatureSK.control_profit_error line 187