OAI/Analysis/HardSphere/Conditioning/SupportedPair.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HardSphere.Comparison.supportedPairline 14 - lemma
OAI.HardSphere.Comparison.supportedPair_mapline 17 - lemma
OAI.HardSphere.Comparison.supportedPair_probabilityline 26 - lemma
OAI.HardSphere.Comparison.map_le_reflectline 34 - lemma
OAI.HardSphere.Comparison.supportedPair_fstline 42 - lemma
OAI.HardSphere.Comparison.supportedPair_sndline 50 - lemma
OAI.HardSphere.Comparison.supportedPair_fst_leline 58 - lemma
OAI.HardSphere.Comparison.supportedPair_snd_leline 66 - lemma
OAI.HardSphere.Comparison.supported_of_marginalsline 74