OAI/Probability/PosteriorReplicas/Gaussian/ConstrainedGaussian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.pairingsDensity line 14
2. lemma OAI.PosteriorReplicas.continuous_pairingsDensity line 19
3. lemma OAI.PosteriorReplicas.gaussian_pairingsDensity line 25
4. lemma OAI.PosteriorReplicas.pairingsDensity_le_zero line 30
5. lemma OAI.PosteriorReplicas.rows_pairings_residual_joint line 44
6. lemma OAI.PosteriorReplicas.rows_pairings_disintegration line 66
7. lemma OAI.PosteriorReplicas.rows_pairings_density line 82
8. lemma OAI.PosteriorReplicas.constrained_gaussian_integral line 94
9. lemma OAI.PosteriorReplicas.pairingsDensity_zero line 112
10. lemma OAI.PosteriorReplicas.rows_pairingsDensity_zero line 118
11. lemma OAI.PosteriorReplicas.continuous_rows_pairingsDensity line 134
12. lemma OAI.PosteriorReplicas.constrained_gaussian_approximation_limit line 145