OAI/Analysis/HardSphere/Comparison/MixtureMoment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.mixed_likelihood_square line 15
2. lemma OAI.HardSphere.Comparison.tag_likelihood_square line 38
3. lemma OAI.HardSphere.Comparison.observed_second_moment line 63
4. lemma OAI.HardSphere.Comparison.observed_kernel_second_moment line 93
5. lemma OAI.HardSphere.Comparison.pairedFactor_swap line 127
6. lemma OAI.HardSphere.Comparison.supportedPair_swap line 139
7. instance OAI.HardSphere.Bridge.targetUniform_finite line 154
8. lemma OAI.HardSphere.Bridge.pairedPathsRaw_eq line 160
9. lemma OAI.HardSphere.Bridge.pairedPathsRaw_support line 168
10. lemma OAI.HardSphere.Bridge.pairedPathsRaw_swap line 175
11. lemma OAI.HardSphere.Bridge.pairedPathsOn_swap line 184