OAI/Analysis/HardSphere/Conditioning/PairFiber.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.pairEvent line 19
2. def OAI.HardSphere.Comparison.frozenCompatible line 22
3. def OAI.HardSphere.Comparison.individualFiber line 26
4. lemma OAI.HardSphere.Comparison.shifted_fiber line 32
5. lemma OAI.HardSphere.Comparison.pairEvent_measurable line 71
6. lemma OAI.HardSphere.Comparison.individualFiber_measurable line 78
7. lemma OAI.HardSphere.Comparison.positive_product_factors line 94
8. lemma OAI.HardSphere.Comparison.conditional_pair_fiber line 101
9. def OAI.HardSphere.noisePairAvoid line 147
10. lemma OAI.HardSphere.noisePairAvoid_measurable line 153
11. lemma OAI.HardSphere.labelInteraction_pair line 160
12. lemma OAI.HardSphere.noise_blockGlue line 181
13. lemma OAI.HardSphere.noise_flag_fiber line 190
14. lemma OAI.HardSphere.recorded_physical_fiber line 207