OAI/Probability/PosteriorReplicas/Regression/LearnerBasics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PosteriorRegression.Learner line 11
2. def OAI.PosteriorRegression.Learner.start line 18
3. def OAI.PosteriorRegression.Learner.run line 23
4. def OAI.PosteriorRegression.Learner.terminal line 36
5. def OAI.PosteriorRegression.Learner.estimate line 42
6. structure OAI.PosteriorRegression.Learner.Admissible line 47
7. def OAI.PosteriorRegression.Learner.success line 59
8. def OAI.PosteriorRegression.Learner.uniformSuccess line 64
9. def OAI.PosteriorRegression.SubquadraticMemory line 71
10. def OAI.PosteriorRegression.FixedQuadraticMemory line 82