OAI/Probability/ClassicalON/PotentialRotation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.SpinSystem.potentialRotation line 13
2. def OAI.ClassicalON.SpinSystem.rotatePotential line 17
3. def OAI.ClassicalON.SpinSystem.potentialOperators line 20
4. theorem OAI.ClassicalON.SpinSystem.gauge_potential_shift line 24
5. theorem OAI.ClassicalON.SpinSystem.potential_shift_Z line 39
6. theorem OAI.ClassicalON.SpinSystem.potential_shift_first line 45
7. theorem OAI.ClassicalON.SpinSystem.potential_shift_second line 58
8. theorem OAI.ClassicalON.SpinSystem.potential_second_response line 71
9. theorem OAI.ClassicalON.SpinSystem.spinRotation_potential_periodic line 83
10. theorem OAI.ClassicalON.SpinSystem.rotatePotential_periodic line 94