OAI/Probability/ProjectionMoments/Streaming.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NoiselessRegression.Learner.riesz_success line 15
2. lemma OAI.NoiselessRegression.prefix_route_mixed_bound line 85
3. lemma OAI.NoiselessRegression.Learner.terminal_eq_forced_of_index line 110
4. lemma OAI.NoiselessRegression.Learner.frozen_fixed_success_bound line 118
5. lemma OAI.NoiselessRegression.Learner.streaming_fixed_success_bound line 159
6. lemma OAI.NoiselessRegression.streamFactor_ofReal line 197
7. lemma OAI.NoiselessRegression.three_mul_four_pow_le line 206
8. theorem OAI.NoiselessRegression.Learner.cap_fixed_stop line 218
9. lemma OAI.NoiselessRegression.Learner.frozen_success_bound_local line 284
10. lemma OAI.NoiselessRegression.Learner.streaming_success_bound_local line 335
11. theorem OAI.NoiselessRegression.Learner.haar_success line 365