OAI/Probability/ParisiFinite/SpinWInv.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

Spin W Inv.

  1. theorem OAI.CoherentFock.spinW_inv line 16
  2. theorem OAI.CoherentFock.spinW_inv' line 20
  3. theorem OAI.CoherentFock.center_probe_product line 25
  4. theorem OAI.CoherentFock.centered_product_phase_bound line 36
  5. theorem OAI.CoherentFock.centered_zero_clock_bound line 59
  6. def OAI.RootSpin.X line 85
  7. def OAI.RootSpin.Y line 86
  8. def OAI.RootSpin.Z line 87
  9. def OAI.RootSpin.R line 88
  10. theorem OAI.RootSpin.X_star line 91
  11. theorem OAI.RootSpin.Y_star line 92
  12. theorem OAI.RootSpin.Z_star line 93
  13. theorem OAI.RootSpin.X_sq line 94
  14. theorem OAI.RootSpin.Y_sq line 95
  15. theorem OAI.RootSpin.Z_sq line 96
  16. theorem OAI.RootSpin.X_unitary line 98
  17. theorem OAI.RootSpin.Y_unitary line 99
  18. theorem OAI.RootSpin.Z_unitary line 100
  19. theorem OAI.RootSpin.R_apply line 102
  20. theorem OAI.RootSpin.R_star line 106
  21. theorem OAI.RootSpin.R_add line 111
  22. theorem OAI.RootSpin.R_zero line 117
  23. theorem OAI.RootSpin.R_unitary line 119
  24. def OAI.RootSpin.hadamard line 124
  25. def OAI.RootSpin.diagUnit line 126
  26. theorem OAI.RootSpin.diagonalization line 132
  27. theorem OAI.RootSpin.exp_X line 138
  28. theorem OAI.RootSpin.R_eq_exp line 146
  29. theorem OAI.RootSpin.R_conjugate_Z line 158
  30. theorem OAI.CoherentFock.rootX_apply line 173
  31. theorem OAI.CoherentFock.rootZ_apply line 177
  32. theorem OAI.CoherentFock.WZ_rootX line 182
  33. theorem OAI.CoherentFock.WZ_rootZ line 189
  34. theorem OAI.CoherentFock.rootR line 195
  35. theorem OAI.CoherentFock.initialization_split line 204
  36. theorem OAI.CoherentFock.initialization_special_norm line 222
  37. theorem OAI.CoherentFock.quarter_conjugate line 232
  38. structure OAI.PointedTree.HilbertData line 243
  39. instance OAI.PointedTree.(instance at line 249) line 249
  40. abbrev OAI.PointedTree.doubleData line 251
  41. abbrev OAI.PointedTree.fockData line 254
  42. abbrev OAI.PointedTree.complexData line 257
  43. def OAI.PointedTree.spinMap line 264
  44. theorem OAI.PointedTree.spinMap_apply line 275
  45. theorem OAI.PointedTree.spinMap_comp line 278
  46. theorem OAI.PointedTree.spinMap_id line 281
  47. theorem OAI.PointedTree.spinMap_root line 285
  48. def OAI.PointedTree.scalarEmbedding line 292
  49. theorem OAI.PointedTree.scalarEmbedding_apply line 298
  50. def OAI.PointedTree.plus line 301
  51. theorem OAI.PointedTree.norm_plus line 303
  52. def OAI.PointedTree.gammaEmbedding line 316
  53. theorem OAI.PointedTree.gammaEmbedding_coherent line 320
  54. def OAI.PointedTree.vacuum line 323
  55. theorem OAI.PointedTree.vacuum_apply line 326
  56. theorem OAI.PointedTree.norm_vacuum line 329
  57. structure OAI.PointedTree.PointedData line 333
  58. instance OAI.PointedTree.(instance at line 336) line 336
  59. instance OAI.PointedTree.(instance at line 337) line 337
  60. instance OAI.PointedTree.(instance at line 338) line 338
  61. instance OAI.PointedTree.(instance at line 339) line 339
  62. def OAI.PointedTree.centered line 343
  63. instance OAI.PointedTree.(instance at line 345) line 345
  64. theorem OAI.PointedTree.mem_centered line 349
  65. structure OAI.PointedTree.PointedMap line 353
  66. def OAI.PointedTree.centeredMap line 357
  67. theorem OAI.PointedTree.centeredMap_coe line 365
  68. abbrev OAI.PointedTree.base line 368
  69. abbrev OAI.PointedTree.next line 373
  70. def OAI.PointedTree.nextMap line 378
  71. def OAI.PointedTree.level line 385
  72. abbrev OAI.PointedTree.Level line 389
  73. abbrev OAI.PointedTree.Mode line 390
  74. def OAI.PointedTree.vac line 392
  75. theorem OAI.PointedTree.norm_vac line 394
  76. def OAI.PointedTree.empty line 397
  77. theorem OAI.PointedTree.empty_vac line 401
  78. def OAI.PointedTree.root line 405
  79. theorem OAI.PointedTree.root_empty line 410
  80. theorem OAI.PointedTree.spinMap_cost line 414
  81. theorem OAI.PointedTree.cost_empty line 423
  82. def OAI.SpinOperators.actEquiv line 433
  83. theorem OAI.SpinOperators.actEquiv_apply line 436
  84. def OAI.PointedTree.spinEquiv line 445
  85. theorem OAI.PointedTree.spinEquiv_apply line 454
  86. theorem OAI.PointedTree.spinFlip_twice line 457
  87. structure OAI.PointedTree.Symmetry line 464
  88. def OAI.PointedTree.Symmetry.centered line 472
  89. theorem OAI.PointedTree.Symmetry.centered_coe line 485
  90. theorem OAI.PointedTree.Symmetry.centered_square line 488
  91. theorem OAI.PointedTree.Symmetry.gamma_square line 491
  92. def OAI.PointedTree.Symmetry.next line 501
  93. def OAI.PointedTree.baseSymmetry line 516
  94. def OAI.PointedTree.symmetry line 528
  95. theorem OAI.PointedTree.symmetry_vac line 532
  96. theorem OAI.PointedTree.symmetry_square line 535
  97. theorem OAI.PointedTree.odd_centered line 540
  98. theorem OAI.CoherentFock.W_neg_cancel_left line 552
  99. def OAI.CoherentFock.costEquiv line 556
  100. theorem OAI.CoherentFock.costEquiv_apply line 569
  101. theorem OAI.CoherentFock.costEquiv_symm_apply line 570
  102. theorem OAI.PointedTree.flipMap_rootZ line 577
  103. theorem OAI.PointedTree.flipMap_rootR line 584
  104. theorem OAI.PointedTree.symmetry_rootZ line 592
  105. theorem OAI.PointedTree.symmetry_rootR line 600
  106. def OAI.PointedTree.rootEquiv line 609
  107. theorem OAI.PointedTree.rootEquiv_apply line 614
  108. theorem OAI.PointedTree.norm_rootZ line 617
  109. structure OAI.PointedTree.EvenUnitary line 622
  110. def OAI.PointedTree.EvenUnitary.ident line 628
  111. def OAI.PointedTree.EvenUnitary.followedBy line 633
  112. theorem OAI.PointedTree.EvenUnitary.symm_commutes line 639
  113. def OAI.PointedTree.EvenUnitary.insertion line 645
  114. theorem OAI.PointedTree.EvenUnitary.insertion_coe line 650
  115. theorem OAI.PointedTree.EvenUnitary.norm_insertion line 653
  116. theorem OAI.PointedTree.EvenUnitary.insertion_odd line 657
  117. def OAI.PointedTree.EvenUnitary.mixer line 664
  118. def OAI.PointedTree.EvenUnitary.cost line 669
  119. theorem OAI.PointedTree.EvenUnitary.cost_insertion line 682