OAI/Probability/SphericalField/Control/Continuity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.controlValue_trial_sub_le line 16
2. lemma OAI.SphericalPerceptron.controlValue_trial_abs_sub_le line 30
3. lemma OAI.SphericalPerceptron.usual_measurable_aemeasurable line 39
4. lemma OAI.SphericalPerceptron.brownian_increment_indep_adapted line 45
5. lemma OAI.SphericalPerceptron.second_order_taylor_bound line 51
6. lemma OAI.SphericalPerceptron.first_order_taylor_bound line 80
7. lemma OAI.SphericalPerceptron.smooth_deriv_lipschitz line 102
8. lemma OAI.SphericalPerceptron.drift_shift_taylor_bound line 109