OAI/Analysis/HardSphere/Allocation/PhysicalTaggedDensity.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HardSphere.Groups.physicalTaggedMixtureline 19 - def
OAI.HardSphere.Groups.physicalTagLikelihoodline 28 - lemma
OAI.HardSphere.Groups.physicalTagLikelihood_measurableline 38 - lemma
OAI.HardSphere.Groups.physicalTagLikelihood_sumline 48 - theorem
OAI.HardSphere.Groups.physicalTaggedMixture_density_supportline 60 - def
OAI.HardSphere.Groups.physicalTaggedReferenceline 119 - theorem
OAI.HardSphere.Groups.physicalTagged_observed_momentline 125