OAI/Probability/ClassicalON/OrthogonalAverage.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ClassicalON.spinOperator_continuousStar line 10
2. abbrev OAI.ClassicalON.SpinOrthogonal line 13
3. instance OAI.ClassicalON.spinOrthogonal_compact line 15
4. instance OAI.ClassicalON.spinOrthogonal_measurableSpace line 21
5. instance OAI.ClassicalON.spinOrthogonal_borelSpace line 22
6. def OAI.ClassicalON.orthogonalLaw line 24
7. instance OAI.ClassicalON.orthogonalLaw_isProbability line 27
8. instance OAI.ClassicalON.orthogonalLaw_isHaar line 33
9. instance OAI.ClassicalON.orthogonalLaw_isRightInvariant line 38
10. def OAI.ClassicalON.orthogonalSpin line 54
11. theorem OAI.ClassicalON.continuous_orthogonalSpin line 57
12. theorem OAI.ClassicalON.orthogonalSpin_mul line 62
13. theorem OAI.ClassicalON.orthogonalSpin_transitive line 66
14. theorem OAI.ClassicalON.orthogonalSpin_preserves line 75
15. theorem OAI.ClassicalON.integral_orthogonalSpin_eq line 79