OAI/Probability/ParisiFinite/SpinMatrix.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Spin Matrix.

  1. abbrev OAI.SeedControl.SpinMatrix line 22
  2. def OAI.SeedControl.x line 24
  3. def OAI.SeedControl.y line 25
  4. def OAI.SeedControl.z line 26
  5. theorem OAI.SeedControl.lie_z_y line 28
  6. theorem OAI.SeedControl.lie_z_lie_z_x line 32
  7. abbrev OAI.SeedControl.Ensemble line 36
  8. def OAI.SeedControl.generatorZ line 38
  9. def OAI.SeedControl.generatorY line 39
  10. def OAI.SeedControl.fieldX line 40
  11. theorem OAI.SeedControl.generator_bracket line 42
  12. theorem OAI.SeedControl.generator_double_bracket line 53
  13. theorem OAI.SeedControl.fieldX_mul_mem line 64
  14. theorem OAI.SeedControl.fieldX_sq_mul_mem line 72
  15. theorem OAI.SeedControl.fieldX_add line 80
  16. theorem OAI.SeedControl.fieldX_const_mul line 86
  17. theorem OAI.SeedControl.weighted_power_mem line 92
  18. theorem OAI.SeedControl.weighted_polynomial_mem line 104
  19. theorem OAI.SeedControl.interpolate_finite_fibers line 120
  20. theorem OAI.SeedControl.common_axis_mem line 137
  21. theorem OAI.SeedControl.exists_generic_slope line 148
  22. theorem OAI.SeedControl.exists_separating_frame line 161
  23. theorem OAI.SeedControl.common_axis_generated line 221
  24. abbrev OAI.QuaternionControl.QField line 242
  25. instance OAI.QuaternionControl.quaternionStarModule line 243
  26. def OAI.QuaternionControl.qX line 249
  27. def OAI.QuaternionControl.qY line 250
  28. def OAI.QuaternionControl.qZ line 251
  29. def OAI.QuaternionControl.gen line 252
  30. def OAI.QuaternionControl.tang line 254
  31. theorem OAI.QuaternionControl.qX_add line 257
  32. theorem OAI.QuaternionControl.qX_smul line 262
  33. theorem OAI.QuaternionControl.bracket_zy line 267
  34. theorem OAI.QuaternionControl.bracket_zx line 274
  35. theorem OAI.QuaternionControl.bracket_yx line 281
  36. theorem OAI.QuaternionControl.double_zx line 288
  37. theorem OAI.QuaternionControl.weighted_mem line 296
  38. theorem OAI.QuaternionControl.weighted_sq_mem line 303
  39. theorem OAI.QuaternionControl.weighted_power_mem line 311
  40. theorem OAI.QuaternionControl.weighted_polynomial_mem line 319
  41. theorem OAI.QuaternionControl.all_X_mem line 328
  42. theorem OAI.QuaternionControl.all_Y_mem line 337
  43. theorem OAI.QuaternionControl.all_Z_mem line 347
  44. def OAI.QuaternionControl.imagProj line 365
  45. theorem OAI.QuaternionControl.imagProj_apply line 371
  46. theorem OAI.QuaternionControl.imagProj_one line 374
  47. theorem OAI.QuaternionControl.gen_skew line 378
  48. theorem OAI.QuaternionControl.tangent_projection_surjective line 384
  49. theorem OAI.QuaternionControl.positive_re_nhds line 394
  50. theorem OAI.QuaternionControl.normSq_of_reachable line 399
  51. theorem OAI.QuaternionControl.unit_positive_imag_injective line 407
  52. theorem OAI.QuaternionControl.locally_exact line 416
  53. theorem OAI.QuaternionControl.exact_imaginary line 433
  54. theorem OAI.PulseControl.pulseValue_map line 467
  55. theorem OAI.PulseControl.zeroClock_map line 480
  56. def OAI.QuaternionControl.flipIJ line 492
  57. theorem OAI.QuaternionControl.flipIJ_apply line 506
  58. def OAI.QuaternionControl.expand line 509
  59. theorem OAI.QuaternionControl.expand_gen line 538
  60. theorem OAI.QuaternionControl.expand_qX line 561
  61. theorem OAI.QuaternionControl.common_X_exact line 572
  62. def OAI.QuaternionControl.rotateIJ line 622
  63. def OAI.QuaternionControl.toPauli line 649