OAI/Probability/GaussianReplacement/StreamLearner.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.Learner.frozen_success_bound line 15

   Also declared: OAI/Probability/GaussianRegression/Success.lean:23 (same declaration text).

2. lemma OAI.NoiselessRegression.Learner.streaming_success_bound line 64

   Also declared: OAI/Probability/GaussianRegression/Success.lean:71 (same declaration text).

3. lemma OAI.NoiselessRegression.sphere_projection_large_eighth line 108
4. lemma OAI.NoiselessRegression.sphere_reflection_success_bound_eighth line 139
5. lemma OAI.NoiselessRegression.Learner.linear_success_bound_three_fifths line 181
6. lemma OAI.NoiselessRegression.Learner.streaming_success_bound_real_three_fifths line 229
7. lemma OAI.NoiselessRegression.precision_from_stream_bound_three_fifths line 254