OAI/Probability/ParisiFinite/ReverseWord.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Reverse Word.

  1. def OAI.TensorWordGram.reverseWord line 40
  2. theorem OAI.TensorWordGram.generators_append line 46
  3. theorem OAI.TensorWordGram.generators_star line 51
  4. theorem OAI.TensorWordGram.weylProduct_append line 66
  5. theorem OAI.TensorWordGram.weylProduct_inner line 74
  6. theorem OAI.TensorWordGram.tensor_word_gram_limit line 93
  7. structure OAI.TensorPackets.Term line 152
  8. def OAI.TensorPackets.term line 159
  9. def OAI.TensorPackets.packet line 162
  10. theorem OAI.TensorPackets.term_apply line 165
  11. theorem OAI.TensorPackets.inner_term line 171
  12. theorem OAI.TensorPackets.packet_nil line 180
  13. theorem OAI.TensorPackets.packet_cons line 181
  14. theorem OAI.TensorPackets.Gram_limit line 184
  15. def OAI.TensorPackets.mixTerm line 208
  16. def OAI.TensorPackets.mixPacket line 211
  17. theorem OAI.TensorPackets.act_term line 214
  18. theorem OAI.TensorPackets.act_packet line 224
  19. def OAI.TensorPackets.prefixTerm line 233
  20. def OAI.TensorPackets.prefixPacket line 235
  21. def OAI.TensorPackets.diagonal line 239
  22. theorem OAI.TensorPackets.diagonal_apply line 242
  23. theorem OAI.TensorPackets.diagonal_term line 245
  24. theorem OAI.TensorPackets.diagonal_packet line 255
  25. inductive OAI.RootTensorCLT.Pulse line 272
  26. def OAI.RootTensorCLT.applyPulse line 278
  27. def OAI.RootTensorCLT.run line 282
  28. def OAI.RootTensorCLT.compilePulse line 286
  29. def OAI.RootTensorCLT.compile line 290
  30. theorem OAI.RootTensorCLT.applyPulse_packet line 294
  31. theorem OAI.RootTensorCLT.run_packet line 301
  32. def OAI.RootTensorCLT.start line 311
  33. theorem OAI.RootTensorCLT.start_packet line 314
  34. def OAI.RootTensorCLT.tensorState line 320
  35. def OAI.RootTensorCLT.tensorPulse line 326
  36. theorem OAI.RootTensorCLT.tensor_step line 331
  37. def OAI.RootTensorCLT.fockState line 338
  38. theorem OAI.RootTensorCLT.fock_step line 341
  39. theorem OAI.RootTensorCLT.root_circuit_Gram_limit line 346
  40. theorem OAI.FiniteTensor.matrixPower_one line 389
  41. theorem OAI.FiniteTensor.matrixPower_mul line 401
  42. theorem OAI.FiniteTensor.matrixPower_star line 411
  43. theorem OAI.FiniteTensor.operatorPower_one line 416
  44. theorem OAI.FiniteTensor.operatorPower_mul line 420
  45. theorem OAI.FiniteTensor.operatorPower_star line 424
  46. theorem OAI.FiniteTensor.operatorPower_unitary line 435
  47. theorem OAI.TensorPackets.diagonal_mul line 449
  48. theorem OAI.TensorPackets.diagonal_one line 455
  49. theorem OAI.TensorPackets.diagonal_star line 459
  50. theorem OAI.TensorPackets.diagonal_unitary line 471
  51. def OAI.FiniteTree.Index line 490
  52. instance OAI.FiniteTree.indexFintype line 494
  53. instance OAI.FiniteTree.indexDecidableEq line 499
  54. instance OAI.FiniteTree.indexNonempty line 504
  55. abbrev OAI.FiniteTree.Space line 509
  56. def OAI.FiniteTree.Tail line 511
  57. instance OAI.FiniteTree.tailNormed line 514
  58. instance OAI.FiniteTree.tailInner line 517
  59. instance OAI.FiniteTree.tailComplete line 520
  60. def OAI.FiniteTree.split line 525
  61. def OAI.FiniteTree.root line 530
  62. theorem OAI.FiniteTree.split_root line 533
  63. theorem OAI.FiniteTree.root_one line 536
  64. theorem OAI.FiniteTree.root_mul line 540
  65. theorem OAI.FiniteTree.root_star line 545
  66. theorem OAI.FiniteTree.root_unitary line 552
  67. def OAI.FiniteTree.vac line 561
  68. theorem OAI.FiniteTree.norm_power_of_norm_one line 565
  69. theorem OAI.FiniteTree.norm_vac line 571
  70. def OAI.FiniteTree.control line 580
  71. theorem OAI.FiniteTree.split_control line 584
  72. theorem OAI.FiniteTree.isometry_conj_unitary line 591
  73. theorem OAI.FiniteTree.control_unitary line 606
  74. def OAI.FiniteTree.spinFlip line 620
  75. theorem OAI.FiniteTree.spinFlip_apply line 624
  76. theorem OAI.FiniteTree.spinFlip_square line 629
  77. theorem OAI.FiniteTree.spinFlip_unitary line 636
  78. theorem OAI.FiniteTree.spinFlip_Z line 640
  79. theorem OAI.FiniteTree.spinFlip_R line 646
  80. def OAI.FiniteTree.flip line 653
  81. theorem OAI.FiniteTree.flip_square line 658
  82. theorem OAI.FiniteTree.flip_unitary line 665
  83. theorem OAI.FiniteTree.split_flip line 672
  84. theorem OAI.FiniteTree.flip_vac line 677
  85. theorem OAI.FiniteTree.flip_rootZ line 691
  86. theorem OAI.FiniteTree.flip_rootR line 703