OAI/Analysis/HardSphere/Comparison/ConditionalTagDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.conditionalTagLikelihood line 16
2. lemma OAI.HardSphere.Comparison.conditionalTagLikelihood_measurable line 20
3. lemma OAI.HardSphere.Comparison.conditionalTagLikelihood_sum line 29
4. lemma OAI.HardSphere.Comparison.tagLikelihood_lintegral line 39
5. theorem OAI.HardSphere.Comparison.conditionalTagged_density line 58
6. lemma OAI.HardSphere.Comparison.tagged_density_of_ae_support line 125
7. lemma OAI.HardSphere.Comparison.conditionalTagged_support line 133
8. theorem OAI.HardSphere.Comparison.tagged_observed_of_density line 147