OAI/Probability/PosteriorReplicas/Measures/DensityTools.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.map_withDensity_comp line 10
2. lemma OAI.PosteriorReplicas.map_withDensity_equiv line 22
3. lemma OAI.PosteriorReplicas.lintegral_fin_prod line 34
4. lemma OAI.PosteriorReplicas.lintegral_finite_prod line 57
5. lemma OAI.PosteriorReplicas.pi_withDensity line 68
6. lemma OAI.PosteriorReplicas.pi_gaussian_density line 82