OAI/Probability/ClassicalON/ComplexWard.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ComplexFourForm line 13
  2. instance OAI.(instance at line 24) line 24
  3. theorem OAI.complex_linear_zero_of_real line 27
  4. theorem OAI.ComplexFourForm.zero_of_real line 47
  5. def OAI.MixedAlgebra.Coeffs.map line 81
  6. theorem OAI.MixedAlgebra.weighted_map line 91
  7. theorem OAI.MixedAlgebra.four_map line 95
  8. theorem OAI.MixedAlgebra.weighted_smul line 100
  9. theorem OAI.MixedAlgebra.four_smul_first line 104
  10. theorem OAI.MixedAlgebra.four_smul_second line 109
  11. theorem OAI.MixedAlgebra.four_smul_third line 114
  12. theorem OAI.MixedAlgebra.four_smul_fourth line 118
  13. theorem OAI.ClassicalON.SpinSystem.integrable_complex_integrand line 127
  14. def OAI.ClassicalON.SpinSystem.averageComplexLinear line 133
  15. def OAI.ClassicalON.SpinSystem.ofRealObservable line 144
  16. theorem OAI.ClassicalON.SpinSystem.averageComplex_ofReal line 147
  17. def OAI.ClassicalON.SpinSystem.complexCoefficients line 155
  18. theorem OAI.ClassicalON.SpinSystem.continuous_complexWeighted line 159
  19. theorem OAI.ClassicalON.SpinSystem.continuous_complexMixedPolynomial line 167
  20. def OAI.ClassicalON.SpinSystem.complexMixedObservable line 174
  21. def OAI.ClassicalON.SpinSystem.complexMixedResponse line 177
  22. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_ofReal line 180
  23. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_add_first line 191
  24. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_smul_first line 200
  25. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_add_second line 208
  26. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_smul_second line 217
  27. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_add_third line 225
  28. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_smul_third line 234
  29. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_add_fourth line 242
  30. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_smul_fourth line 251
  31. def OAI.ClassicalON.SpinSystem.complexEnergy line 259
  32. theorem OAI.ClassicalON.SpinSystem.continuous_complexEnergy line 264
  33. theorem OAI.ClassicalON.SpinSystem.complexEnergy_ofReal line 269
  34. theorem OAI.ClassicalON.SpinSystem.complexEnergy_add line 277
  35. theorem OAI.ClassicalON.SpinSystem.complexEnergy_smul line 283
  36. theorem OAI.ClassicalON.SpinSystem.continuous_complexSecondPolynomial line 289
  37. def OAI.ClassicalON.SpinSystem.complexSecondObservable line 294
  38. def OAI.ClassicalON.SpinSystem.complexSecondResponse line 297
  39. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_ofReal line 300
  40. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_add_left line 316
  41. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_symm line 332
  42. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_add_right line 343
  43. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_smul_left line 348
  44. theorem OAI.ClassicalON.SpinSystem.complexSecondResponse_smul_right line 361
  45. def OAI.ClassicalON.SpinSystem.complexCross line 367
  46. theorem OAI.ClassicalON.SpinSystem.complexCross_ofReal line 371
  47. theorem OAI.ClassicalON.SpinSystem.differential_ofReal line 378
  48. theorem OAI.ClassicalON.SpinSystem.complexCross_add_left line 384
  49. theorem OAI.ClassicalON.SpinSystem.complexCross_smul_left line 391
  50. theorem OAI.ClassicalON.SpinSystem.complexCross_add_right line 398
  51. theorem OAI.ClassicalON.SpinSystem.complexCross_smul_right line 405
  52. theorem OAI.ClassicalON.SpinSystem.complexDifferential_add line 412
  53. theorem OAI.ClassicalON.SpinSystem.complexDifferential_smul line 419
  54. def OAI.ClassicalON.SpinSystem.complexWardDefect line 425
  55. theorem OAI.ClassicalON.SpinSystem.complexWardDefect_real line 471
  56. theorem OAI.ClassicalON.SpinSystem.complexMixedResponse_ward line 484