OAI/Probability/PosteriorReplicas/Gaussian/GaussianSmallBall.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.gaussian_density_ball_lower line 13
2. lemma OAI.PosteriorReplicas.gaussian_density_ball_upper line 33
3. lemma OAI.PosteriorReplicas.gaussian_closedBall_ratio line 50
4. lemma OAI.PosteriorReplicas.gaussian_normalized_inverse_moment line 83
5. lemma OAI.PosteriorReplicas.gaussian_inverse_norm_moment line 104