OAI/Probability/ClassicalON/MixedWard.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MixedAlgebra.weighted_const_mul line 13
  2. theorem OAI.ClassicalON.SpinSystem.planeEnergy_two line 25
  3. theorem OAI.ClassicalON.SpinSystem.planeEnergy_three line 39
  4. theorem OAI.ClassicalON.SpinSystem.planeEnergy_four_even line 56
  5. theorem OAI.ClassicalON.SpinSystem.operator_smul_pow line 79
  6. theorem OAI.ClassicalON.SpinSystem.energy_scaled_power line 89
  7. def OAI.ClassicalON.SpinSystem.averageLinear line 98
  8. theorem OAI.ClassicalON.SpinSystem.averageLinear_apply line 103
  9. theorem OAI.ClassicalON.SpinSystem.continuous_fourthPolynomial line 109
  10. def OAI.ClassicalON.SpinSystem.fourthObservable line 114
  11. theorem OAI.ClassicalON.SpinSystem.average_fourthObservable line 117
  12. theorem OAI.ClassicalON.SpinSystem.continuous_weighted_coefficient line 121
  13. theorem OAI.ClassicalON.SpinSystem.continuous_mixedPolynomial line 132
  14. def OAI.ClassicalON.SpinSystem.mixedObservable line 138
  15. def OAI.ClassicalON.SpinSystem.mixedResponse line 141
  16. theorem OAI.ClassicalON.SpinSystem.fourthObservable_even line 145
  17. theorem OAI.ClassicalON.SpinSystem.mixedResponse_diagonal line 183
  18. theorem OAI.ClassicalON.SpinSystem.mixedResponse_polarize_a line 208
  19. theorem OAI.ClassicalON.SpinSystem.mixedResponse_polarize_b line 218
  20. theorem OAI.ClassicalON.SpinSystem.continuous_secondPolynomial line 229
  21. def OAI.ClassicalON.SpinSystem.secondObservable line 234
  22. theorem OAI.ClassicalON.SpinSystem.secondObservable_average line 237
  23. theorem OAI.ClassicalON.SpinSystem.secondObservable_add_left line 241
  24. theorem OAI.ClassicalON.SpinSystem.secondObservable_symm line 259
  25. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_add_left line 266
  26. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_symm line 271
  27. theorem OAI.ClassicalON.SpinSystem.secondAxisResponse_add_right line 275
  28. theorem OAI.ClassicalON.SpinSystem.differential_add line 281
  29. theorem OAI.ClassicalON.SpinSystem.crossForm_add_left line 288
  30. theorem OAI.ClassicalON.SpinSystem.crossForm_add_right line 295
  31. theorem OAI.ClassicalON.SpinSystem.mixedResponse_a_polarized line 301
  32. theorem OAI.ClassicalON.SpinSystem.mixedResponse_ward line 319