OAI/Probability/Subsphere/Estimates/HalfPrecision.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.sphere_projection_eighth line 14
2. lemma OAI.SubsphereRegression.three_sets_bound line 46
3. lemma OAI.SubsphereRegression.sphere_three_orbit_bound line 63
4. lemma OAI.SubsphereRegression.Learner.half_linear_success_bound line 126
5. lemma OAI.SubsphereRegression.Learner.streaming_success_bound_half_real line 179
6. lemma OAI.SubsphereRegression.precision_from_stream_bound_half_aux line 204
7. theorem OAI.SubsphereRegression.half_precision_old_model line 289
8. theorem OAI.SubsphereCurrent.half_precision line 338