OAI/Probability/PosteriorReplicas/Measures/EqualApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.equalApprox line 11
2. def OAI.PosteriorReplicas.smoothedTail line 17
3. lemma OAI.PosteriorReplicas.equalApprox_cons line 22
4. lemma OAI.PosteriorReplicas.smoothedTail_representation line 32
5. lemma OAI.PosteriorReplicas.smoothedTail_bound line 61
6. lemma OAI.PosteriorReplicas.smoothedTail_limit line 81
7. lemma OAI.PosteriorReplicas.equalApprox_left_limit line 143