OAI/Probability/ParisiFinite/Space.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

Space.

  1. abbrev OAI.HilbertPair.Space line 26
  2. def OAI.HilbertPair.inl line 28
  3. def OAI.HilbertPair.inr line 32
  4. theorem OAI.HilbertPair.inl_apply line 36
  5. theorem OAI.HilbertPair.inr_apply line 37
  6. theorem OAI.HilbertPair.inl_inner_inr line 38
  7. theorem OAI.HilbertPair.inr_inner_inl line 39
  8. theorem OAI.HilbertPair.inl_add_inr line 41
  9. def OAI.HilbertPair.map line 46
  10. theorem OAI.HilbertPair.map_apply line 52
  11. theorem OAI.HilbertPair.map_inl line 55
  12. theorem OAI.HilbertPair.map_inr line 58
  13. def OAI.HilbertPair.congr line 61
  14. theorem OAI.HilbertPair.congr_apply line 76
  15. abbrev OAI.SeededTree.External line 86
  16. abbrev OAI.SeededTree.gaussianNode line 87
  17. abbrev OAI.SeededTree.base line 92
  18. abbrev OAI.SeededTree.next line 93
  19. abbrev OAI.SeededTree.centeredData line 95
  20. abbrev OAI.SeededTree.pairData line 98
  21. abbrev OAI.SeededTree.nextTop line 101
  22. def OAI.SeededTree.topData line 104
  23. abbrev OAI.SeededTree.TopMode line 107
  24. abbrev OAI.SeededTree.level line 108
  25. abbrev OAI.SeededTree.Level line 109
  26. abbrev OAI.SeededTree.Mode line 110
  27. def OAI.SeededTree.vac line 111
  28. theorem OAI.SeededTree.norm_vac line 112
  29. def OAI.SeededTree.gaussianMap line 115
  30. def OAI.SeededTree.nextMap line 121
  31. def OAI.SeededTree.empty line 124
  32. theorem OAI.SeededTree.empty_vac line 128
  33. def OAI.SeededTree.topStep line 131
  34. theorem OAI.SeededTree.empty_apply line 135
  35. def OAI.SeededTree.external line 138
  36. def OAI.SeededTree.endogenous line 142
  37. theorem OAI.SeededTree.topStep_external line 144
  38. theorem OAI.SeededTree.topStep_endogenous line 150
  39. theorem OAI.SeededTree.external_inner_endogenous line 154
  40. def OAI.SeededTree.gaussianSymmetry line 158
  41. def OAI.SeededTree.externalFlip line 177
  42. theorem OAI.SeededTree.externalFlip_apply line 178
  43. def OAI.SeededTree.nextSymmetry line 180
  44. def OAI.SeededTree.symmetry line 187
  45. def OAI.SeededTree.topFlip line 191
  46. theorem OAI.SeededTree.symmetry_apply line 195
  47. theorem OAI.SeededTree.topFlip_external line 198
  48. theorem OAI.SeededTree.topFlip_endogenous line 209
  49. theorem OAI.SeededTree.symmetry_vac line 215
  50. def OAI.SeededTree.root line 217
  51. theorem OAI.SeededTree.root_apply line 219
  52. theorem OAI.SeededTree.symmetry_rootZ line 222
  53. theorem OAI.SeededTree.symmetry_rootR line 229
  54. def OAI.SeededTree.rootEquiv line 236
  55. theorem OAI.SeededTree.rootEquiv_apply line 238
  56. theorem OAI.SeededTree.norm_rootZ line 240
  57. structure OAI.SeededTree.EvenUnitary line 243
  58. def OAI.SeededTree.EvenUnitary.ident line 249
  59. def OAI.SeededTree.EvenUnitary.followedBy line 253
  60. theorem OAI.SeededTree.EvenUnitary.symm_commutes line 259
  61. def OAI.SeededTree.EvenUnitary.insertion line 264
  62. theorem OAI.SeededTree.EvenUnitary.insertion_coe line 268
  63. theorem OAI.SeededTree.EvenUnitary.norm_insertion line 270
  64. theorem OAI.SeededTree.EvenUnitary.insertion_odd line 273
  65. def OAI.SeededTree.EvenUnitary.mixer line 279
  66. def OAI.SeededTree.EvenUnitary.pulse line 283
  67. theorem OAI.SeededTree.EvenUnitary.pulse_apply line 293
  68. def OAI.SeededTree.EvenUnitary.seed line 297
  69. def OAI.SeededTree.EvenUnitary.cost line 300
  70. theorem OAI.SeededTree.root_empty line 310
  71. theorem OAI.SeededTree.pulse_empty line 315
  72. def OAI.SeededTree.EvenUnitary.Compatible line 322
  73. theorem OAI.SeededTree.EvenUnitary.Compatible.symm_apply line 325
  74. theorem OAI.SeededTree.EvenUnitary.Compatible.insertion line 331
  75. theorem OAI.SeededTree.EvenUnitary.Compatible.followedBy line 338
  76. theorem OAI.SeededTree.EvenUnitary.compatible_ident line 345
  77. theorem OAI.SeededTree.EvenUnitary.compatible_mixer line 347
  78. theorem OAI.SeededTree.EvenUnitary.compatible_pulse line 352
  79. theorem OAI.SeededTree.EvenUnitary.compatible_seed line 359
  80. theorem OAI.SeededTree.EvenUnitary.compatible_cost line 362
  81. theorem OAI.SeededTree.EvenUnitary.pulse_insertion line 368
  82. inductive OAI.SeededTree.Gate line 382
  83. def OAI.SeededTree.circuit line 388
  84. theorem OAI.SeededTree.circuit_compatible line 395
  85. theorem OAI.SeededTree.circuit_insertion_empty line 415
  86. def OAI.SeededTree.rootShift line 421
  87. theorem OAI.SeededTree.rootShift_coe line 440
  88. theorem OAI.SeededTree.rootShift_empty line 443
  89. def OAI.SeededTree.treeEnergy line 452
  90. theorem OAI.SeededTree.treeEnergy_empty line 454
  91. theorem OAI.SeededTree.abs_treeEnergy_le line 460
  92. def OAI.SeededTree.value line 466
  93. theorem OAI.SeededTree.value_eq_height line 468
  94. theorem OAI.SeededTree.abs_value_le line 475
  95. def OAI.CoherentFock.PacketForm line 486
  96. theorem OAI.CoherentFock.PacketForm.inner line 494
  97. theorem OAI.CoherentFock.PacketForm.zero line 506
  98. theorem OAI.CoherentFock.PacketForm.add line 512
  99. theorem OAI.CoherentFock.PacketForm.smul line 528
  100. theorem OAI.CoherentFock.PacketForm.neg line 538
  101. theorem OAI.CoherentFock.PacketForm.vacuum line 542
  102. theorem OAI.CoherentFock.PacketForm.root line 550
  103. theorem OAI.CoherentFock.PacketForm.pulse line 564
  104. def OAI.SeededTree.TopRegular line 604
  105. def OAI.SeededTree.PacketRegular line 609
  106. theorem OAI.SeededTree.TopRegular.inner line 614
  107. theorem OAI.SeededTree.TopRegular.zero line 637
  108. theorem OAI.SeededTree.TopRegular.add line 642
  109. theorem OAI.SeededTree.TopRegular.smul line 648
  110. theorem OAI.SeededTree.TopRegular.neg line 655
  111. theorem OAI.SeededTree.TopRegular.external line 659
  112. theorem OAI.SeededTree.TopRegular.endogenous line 665
  113. theorem OAI.SeededTree.PacketRegular.inner line 675
  114. theorem OAI.SeededTree.PacketRegular.zero line 680
  115. theorem OAI.SeededTree.PacketRegular.add line 682
  116. theorem OAI.SeededTree.PacketRegular.smul line 685
  117. theorem OAI.SeededTree.PacketRegular.neg line 689
  118. theorem OAI.SeededTree.PacketRegular.vac line 692
  119. theorem OAI.SeededTree.PacketRegular.root line 695
  120. theorem OAI.SeededTree.PacketRegular.pulse line 699