OAI/Probability/SKValue/Processes/Feedback.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.meshControl line 15
2. lemma OAI.SKValue.progressive_interval line 19
3. lemma OAI.SKValue.meshControl_progressive line 41
4. lemma OAI.SKValue.mesh_intervals_disjoint line 49
5. lemma OAI.SKValue.meshControl_eq line 64
6. lemma OAI.SKValue.meshControl_bound line 74
7. lemma OAI.SKValue.meshControl_momentIntegral line 88
8. lemma OAI.SKValue.monotone_interval_quadrature line 122
9. lemma OAI.SKValue.meshControl_quadrature line 140
10. lemma OAI.SKValue.coupled_euler_past_measurable line 184
11. lemma OAI.SKValue.coupled_euler_drift_sum line 216
12. def OAI.SKValue.feedbackControl line 233
13. lemma OAI.SKValue.ValueStrip.feedback_progressive line 238
14. lemma OAI.SKValue.ValueStrip.feedback_bound line 251
15. lemma OAI.SKValue.ValueStrip.feedback_state_error line 257
16. lemma OAI.SKValue.ValueStrip.feedback_energy_error line 271