OAI/Probability/ClassicalON/RotationInequality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.SpinSystem.complexSecondBilin line 15
2. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_neg_neg line 27
3. theorem OAI.ClassicalON.SpinSystem.commutatorForm_antisymm line 33
4. theorem OAI.ClassicalON.SpinSystem.commutatorForm_conj line 40
5. theorem OAI.ClassicalON.SpinSystem.commutatorForm_bound_right line 48
6. theorem OAI.ClassicalON.SpinSystem.commutatorForm_bound line 63
7. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_commutator line 75
8. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_paired line 89
9. theorem OAI.ClassicalON.SpinSystem.rotation_family_bound line 115