OAI/Probability/ClassicalON/SpinIsotropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.coordinateRotation line 13
2. theorem OAI.ClassicalON.coordinateRotation_apply line 18
3. theorem OAI.ClassicalON.freeSpinReference_rotation line 23
4. theorem OAI.ClassicalON.freeSpinEnergy_rotation line 29
5. def OAI.ClassicalON.coordinateSpinProduct line 38
6. theorem OAI.ClassicalON.continuous_coordinateSpinProduct line 42
7. theorem OAI.ClassicalON.coordinateSpinMean_eq line 47
8. theorem OAI.ClassicalON.innerSpinMean_eq_coordinate line 63