OAI/Probability/PosteriorReplicas/Learners/LearnerModelBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PosteriorRegression.Learner.UniformAdmissible line 12
2. lemma OAI.PosteriorRegression.Learner.Admissible.uniformAdmissible line 20
3. lemma OAI.PosteriorRegression.Learner.UniformAdmissible.angularSuccess_nullMeasurable line 30
4. lemma OAI.PosteriorRegression.Learner.UniformAdmissible.linear_success_bound line 41
5. lemma OAI.PosteriorRegression.Learner.UniformAdmissible.streaming_success_bound line 87
6. lemma OAI.PosteriorRegression.Learner.UniformAdmissible.streaming_success_bound_real line 111
7. def OAI.PosteriorRegression.UniformSubquadraticMemory line 136
8. lemma OAI.PosteriorRegression.source_fixed_quadratic_memory line 146
9. theorem OAI.PosteriorRegression.source_subquadratic_memory line 167