OAI/Probability/ClassicalON/SecondGauge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_integral line 14
2. theorem OAI.ClassicalON.SpinSystem.Z_axis_add_gradient line 29
3. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_gradient_diag line 45
4. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_gradient_right line 68
5. theorem OAI.ClassicalON.SpinSystem.differential_add_complex line 85
6. theorem OAI.ClassicalON.SpinSystem.differential_smul_complex line 92
7. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_gradient_right line 97
8. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_add_gradient_right line 119
9. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_add_gradients line 124