OAI/Analysis/HardSphere/Comparison/ConditionalLikelihood.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.partialNormalizer_le_one line 18
2. lemma OAI.HardSphere.Comparison.measurable_partialNormalizer line 25
3. lemma OAI.HardSphere.Comparison.UniformInsertionOn.mono line 30
4. lemma OAI.HardSphere.Comparison.checkNormalizer_pos_on line 34
5. lemma OAI.HardSphere.Comparison.checkNormalizer_union_lower_on line 43
6. lemma OAI.HardSphere.Comparison.isProbabilityMeasure_compProd_of_mass line 53
7. lemma OAI.HardSphere.Comparison.conditionalDensity_overlap_bound line 70
8. lemma OAI.HardSphere.Comparison.finite_normalizer_cancellation line 92
9. lemma OAI.HardSphere.Comparison.partialNormalizer_ge_far line 118
10. def OAI.HardSphere.Comparison.conditionalLikelihood line 144
11. lemma OAI.HardSphere.Comparison.measurable_conditionalLikelihood line 149
12. theorem OAI.HardSphere.Comparison.conditional_cancellation line 157
13. lemma OAI.HardSphere.Comparison.partialNormalizer_updateFinset line 299
14. lemma OAI.HardSphere.Comparison.partialNormalizer_le_outside line 307
15. lemma OAI.HardSphere.Comparison.conditionalDensity_reference_support line 317
16. theorem OAI.HardSphere.Comparison.conditionalLikelihood_marginal line 336
17. def OAI.HardSphere.Comparison.referenceMeasure line 401
18. lemma OAI.HardSphere.Comparison.referenceMeasure_mass line 407
19. lemma OAI.HardSphere.Comparison.referenceMeasure_probability line 416