OAI/Probability/ClassicalON/SpinCorrelation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.firstSpinProduct line 13
2. theorem OAI.ClassicalON.continuous_firstSpinProduct line 16
3. theorem OAI.ClassicalON.cylindrical_firstSpinProduct line 21
4. theorem OAI.ClassicalON.integral_cylinder_firstSpin line 27
5. theorem OAI.ClassicalON.firstSpinMean_eq_jointBondMean line 53
6. theorem OAI.ClassicalON.jointBondMean_nonneg line 67
7. theorem OAI.ClassicalON.jointBondMean_mono line 74
8. theorem OAI.ClassicalON.firstSpinMean_bounds line 84