OAI/Probability/PosteriorReplicas/Regression/AffineTubes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PosteriorRegression.exists_affine_tube_cover line 19
2. theorem OAI.PosteriorRegression.HasLocalMassBound.affine_tube line 51
3. lemma OAI.PosteriorRegression.tube_radius_factors line 81
4. theorem OAI.PosteriorRegression.HasLocalMassBound.affine_tube_pow line 88
5. theorem OAI.PosteriorRegression.HasLocalMassBound.affine_inverse_moment line 103
6. theorem OAI.PosteriorRegression.HasLocalMassBound.affine_null line 116