OAI/Probability/SphericalField/Control/StepError.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.heatLog_control_step_error line 16
2. lemma OAI.SphericalPerceptron.usualBrownianSigma_mono line 85
3. lemma OAI.SphericalPerceptron.brownianEval_usual_measurable line 91
4. lemma OAI.SphericalPerceptron.progressive_prefix_integral_measurable line 100
5. lemma OAI.SphericalPerceptron.progressive_interval_integral_aemeasurable line 116
6. def OAI.SphericalPerceptron.controlledPrefix line 125
7. lemma OAI.SphericalPerceptron.controlledPrefix_usual_measurable line 128
8. def OAI.SphericalPerceptron.timeSpan line 133
9. lemma OAI.SphericalPerceptron.timeSpan_coe line 135
10. lemma OAI.SphericalPerceptron.timeSpan_le_one line 138