OAI/Probability/ClassicalON/CylindricalLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.cylinderLaw line 10
2. instance OAI.ClassicalON.cylinderLaw_isProbability line 11
3. def OAI.ClassicalON.sphericalAmplitudeLaw line 14
4. instance OAI.ClassicalON.sphericalAmplitudeLaw_isProbability line 15
5. theorem OAI.ClassicalON.integral_signLaw line 18
6. theorem OAI.ClassicalON.integral_cylinderLaw line 22
7. theorem OAI.ClassicalON.cylinder_orbit_average line 26
8. theorem OAI.ClassicalON.integral_sphere_orbit line 51
9. theorem OAI.ClassicalON.integral_sphere_cylinder line 66
10. theorem OAI.ClassicalON.cylindricalSpin_preserves line 79