OAI/Probability/ParisiFinite/FlipStar.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Flip Star.

  1. theorem OAI.FiniteTree.flip_star line 39
  2. structure OAI.FiniteTree.Even line 47
  3. def OAI.FiniteTree.Even.ident line 55
  4. def OAI.FiniteTree.Even.followedBy line 60
  5. def OAI.FiniteTree.Even.mixer line 66
  6. theorem OAI.FiniteTree.Even.star_commutes line 74
  7. def OAI.FiniteTree.Even.observable line 79
  8. theorem OAI.FiniteTree.Even.observable_star line 82
  9. theorem OAI.FiniteTree.Even.observable_unitary line 85
  10. theorem OAI.FiniteTree.Even.norm_observable line 89
  11. theorem OAI.FiniteTree.Even.observable_odd line 92
  12. theorem OAI.FiniteTree.Even.observable_centered line 112
  13. def OAI.FiniteTree.Even.generator line 126
  14. theorem OAI.FiniteTree.Even.generator_neg line 129
  15. theorem OAI.FiniteTree.Even.generator_star line 133
  16. theorem OAI.FiniteTree.Even.norm_generator line 139
  17. theorem OAI.FiniteTree.Even.generator_centered line 142
  18. def OAI.FiniteTree.Even.exponential line 146
  19. theorem OAI.FiniteTree.Even.exponential_unitary line 149
  20. theorem OAI.FiniteTree.Even.generator_odd line 157
  21. theorem OAI.FiniteTree.Even.exponential_odd line 164
  22. theorem OAI.FiniteTree.spinFlip_diagonal line 182
  23. theorem OAI.FiniteTree.flip_control line 192
  24. theorem OAI.FiniteTree.Even.cost_blocks_flip line 207
  25. def OAI.FiniteTree.Even.cost line 214
  26. def OAI.FiniteTree.ordinary line 223
  27. theorem OAI.FiniteTree.ordinary_zero_level line 230
  28. theorem OAI.RootTensorCLT.run_nil line 254
  29. theorem OAI.RootTensorCLT.run_cons line 255
  30. theorem OAI.RootTensorCLT.run_append line 258
  31. def OAI.RootTensorCLT.adjointPulse line 264
  32. def OAI.RootTensorCLT.adjointProgram line 268
  33. theorem OAI.RootTensorCLT.applyPulse_adjoint line 274
  34. theorem OAI.RootTensorCLT.run_adjoint line 286
  35. theorem OAI.RootTensorCLT.weyl_star line 295
  36. theorem OAI.RootTensorCLT.tensorPulse_star line 304
  37. abbrev OAI.FiniteTree.Label line 323
  38. def OAI.FiniteTree.negateLabel line 325
  39. theorem OAI.FiniteTree.negateLabel_involutive line 327
  40. def OAI.FiniteTree.childGenerator line 332
  41. def OAI.FiniteTree.childDirection line 335
  42. def OAI.FiniteTree.program line 340
  43. theorem OAI.FiniteTree.generator_scaled line 345
  44. theorem OAI.FiniteTree.cost_tensorPulse line 351
  45. theorem OAI.FiniteTree.split_ordinary line 361
  46. theorem OAI.FiniteTree.weyl_cost_program line 381
  47. theorem OAI.FiniteTree.limiting_ordinary line 388
  48. def OAI.RootTensorCLT.Pulse.labels line 422
  49. def OAI.RootTensorCLT.labels line 428
  50. theorem OAI.RootTensorCLT.control_mem_labels line 432
  51. theorem OAI.RootTensorCLT.labels_tail line 438
  52. theorem OAI.RootTensorCLT.run_congr_labels line 445
  53. def OAI.RootTensorCLT.negClosure line 461
  54. theorem OAI.RootTensorCLT.mem_negClosure line 464
  55. def OAI.RootTensorCLT.mask line 478
  56. theorem OAI.RootTensorCLT.root_circuit_Gram_local_limit line 483
  57. def OAI.FiniteTree.insertion line 550
  58. def OAI.FiniteTree.insertionProgram line 553
  59. theorem OAI.FiniteTree.childGenerator_neg line 556
  60. theorem OAI.FiniteTree.childGenerator_star line 560
  61. theorem OAI.FiniteTree.childDirection_neg line 564
  62. theorem OAI.FiniteTree.conj_split_ordinary line 568
  63. theorem OAI.FiniteTree.split_ordinary_star line 577
  64. theorem OAI.FiniteTree.split_insertion line 588
  65. theorem OAI.FiniteTree.limiting_insertion line 600
  66. theorem OAI.FiniteTree.insertion_zero line 612
  67. theorem OAI.FiniteTree.child_second_moment line 620