OAI/Probability/SphericalField/Control/Intervals.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.timeLaw_real_Ioc line 16
2. lemma OAI.SphericalPerceptron.timeLaw_integral_const_Ioc line 21
3. lemma OAI.SphericalPerceptron.bounded_control_integrable line 26
4. lemma OAI.SphericalPerceptron.controlledPrefix_increment line 32
5. lemma OAI.SphericalPerceptron.bounded_interval_drift line 47
6. def OAI.SphericalPerceptron.intervalControlCost line 63
7. lemma OAI.SphericalPerceptron.intervalControlCost_nonneg line 66
8. lemma OAI.SphericalPerceptron.intervalControlCost_aemeasurable line 69
9. lemma OAI.SphericalPerceptron.intervalControlCost_le_bound line 74
10. lemma OAI.SphericalPerceptron.intervalControlCost_integrable line 88
11. lemma OAI.SphericalPerceptron.interval_square_completion line 97
12. lemma OAI.SphericalPerceptron.brownian_increment_timeSpan line 120
13. lemma OAI.SphericalPerceptron.brownian_control_cell_upper line 131