OAI/Probability/PosteriorReplicas/Regression/SphereBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorRegression.unitBallLaw line 17
2. def OAI.PosteriorRegression.sphereLaw line 20
3. lemma OAI.PosteriorRegression.unitBallLaw_closedBall line 24
4. lemma OAI.PosteriorRegression.unitBallLaw_local line 36
5. lemma OAI.PosteriorRegression.unitBallLaw_support line 41
6. instance OAI.PosteriorRegression.unitBallLaw_probability line 47
7. instance OAI.PosteriorRegression.sphereLaw_probability line 55
8. lemma OAI.PosteriorRegression.sphereLaw_apply line 63
9. lemma OAI.PosteriorRegression.sphereLaw_cap_raw line 85