OAI/Probability/ClassicalON/RotationWork.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MixedAlgebra.weighted line 15
  2. theorem OAI.MixedAlgebra.weighted_add line 17
  3. theorem OAI.MixedAlgebra.weighted_neg line 21
  4. structure OAI.MixedAlgebra.Coeffs line 24
  5. def OAI.MixedAlgebra.four line 34
  6. theorem OAI.MixedAlgebra.four_add_first line 51
  7. theorem OAI.MixedAlgebra.four_add_second line 56
  8. theorem OAI.MixedAlgebra.four_swap_first_third line 61
  9. theorem OAI.MixedAlgebra.four_swap_second_fourth line 67
  10. theorem OAI.MixedAlgebra.four_add_third line 78
  11. theorem OAI.MixedAlgebra.four_add_fourth line 83
  12. theorem OAI.MixedAlgebra.four_polarize_a line 88
  13. theorem OAI.MixedAlgebra.four_polarize_b line 93
  14. theorem OAI.MixedAlgebra.four_diagonal line 103
  15. def OAI.bell4 line 119
  16. theorem OAI.bell4_even line 121
  17. theorem OAI.ClassicalON.SpinSystem.fourthResponse_plane_even line 134
  18. theorem OAI.ClassicalON.SpinSystem.fourthResponse_axisGradient line 222
  19. def OAI.ClassicalON.SpinSystem.localCoefficient line 250
  20. theorem OAI.ClassicalON.SpinSystem.energy_weighted line 255
  21. def OAI.ClassicalON.SpinSystem.mixedCoefficients line 264
  22. def OAI.ClassicalON.SpinSystem.differential line 275
  23. theorem OAI.ClassicalON.SpinSystem.planarGradient_eq line 279
  24. theorem OAI.ClassicalON.SpinSystem.planeEnergy_one line 286