OAI/Probability/ParisiFinite/ParamGate.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Param Gate.

  1. inductive OAI.SeededTree.ParamGate line 23
  2. def OAI.SeededTree.ParamGate.eval line 28
  3. def OAI.SeededTree.ParamGate.regular line 34
  4. def OAI.SeededTree.evalWord line 40
  5. theorem OAI.SeededTree.rootEquiv_symm_apply line 43
  6. theorem OAI.SeededTree.seed_topRegular line 50
  7. theorem OAI.SeededTree.circuit_packetRegular line 56
  8. theorem OAI.SeededTree.circuit_insertion_packetRegular line 120
  9. theorem OAI.SeededTree.analyticAt_insertionGram line 127
  10. theorem OAI.CoherentFock.spinMap_spinPacket line 141
  11. theorem OAI.CoherentFock.PacketForm.gamma line 149
  12. theorem OAI.SeededTree.topStep_empty_regular line 169
  13. theorem OAI.SeededTree.PacketRegular.empty line 197
  14. theorem OAI.SeededTree.PacketRegular.finsetSum line 201
  15. theorem OAI.SeededTree.analyticAt_treeEnergy line 215
  16. theorem OAI.SeededTree.analyticAt_value line 229
  17. def OAI.SeededTree.centerAccumulator line 240
  18. theorem OAI.SeededTree.centerAccumulator_packetRegular line 244
  19. def OAI.SeededTree.formalVisibility line 259
  20. theorem OAI.SeededTree.analyticAt_formalVisibility line 265
  21. theorem OAI.SeededTree.EvenUnitary.ext line 284
  22. theorem OAI.SeededTree.EvenUnitary.followedBy_ident line 290
  23. theorem OAI.SeededTree.EvenUnitary.mixer_zero line 296
  24. theorem OAI.SeededTree.EvenUnitary.seed_zero line 304
  25. theorem OAI.SeededTree.EvenUnitary.cost_zero line 313
  26. def OAI.SeededTree.Gate.IsZero line 321
  27. theorem OAI.SeededTree.circuit_zero_prefix line 328
  28. def OAI.SeededTree.ell line 356
  29. theorem OAI.SeededTree.norm_ell line 357
  30. def OAI.SeededTree.initializationAngles line 359
  31. def OAI.SeededTree.initializationDisplacement line 361
  32. theorem OAI.SeededTree.initializationDisplacement_eq line 364
  33. theorem OAI.SeededTree.initializationDisplacement_norm_sq line 372
  34. def OAI.SeededTree.initializationWord line 379
  35. theorem OAI.SeededTree.initialization_insertion_coe line 383
  36. theorem OAI.SeededTree.inner_initialization_initial line 398
  37. def OAI.SeededTree.initializationParam line 425
  38. theorem OAI.SeededTree.eval_initializationParam line 429
  39. theorem OAI.SeededTree.initializationParam_regular line 432
  40. theorem OAI.SeededTree.evalWord_append line 441
  41. theorem OAI.SeededTree.centerAccumulator_zero line 445
  42. theorem OAI.SeededTree.formalVisibility_initialization line 453
  43. inductive OAI.SeededTree.IndexedGate line 471
  44. def OAI.SeededTree.IndexedGate.param line 476
  45. theorem OAI.SeededTree.IndexedGate.param_regular line 481
  46. theorem OAI.SeededTree.IndexedGate.param_zero line 495
  47. def OAI.SeededTree.indexedWord line 499
  48. theorem OAI.SeededTree.indexedWord_regular line 502
  49. theorem OAI.SeededTree.indexedWord_zero line 508
  50. def OAI.SeededTree.indexedTime line 516
  51. theorem OAI.SeededTree.indexedTime_regular line 518
  52. theorem OAI.SeededTree.indexedTime_zero line 522
  53. theorem OAI.SeededTree.indexedVisibility_zero line 526
  54. theorem OAI.SeededTree.exists_visible_perturbation line 541
  55. def OAI.SeededTree.ordinaryLift line 603
  56. theorem OAI.SeededTree.ordinaryLift_vac line 607
  57. theorem OAI.SeededTree.ordinaryLift_root line 611
  58. theorem OAI.SeededTree.ordinaryLift_cost line 617
  59. def OAI.SeededTree.LiftCompatible line 624
  60. theorem OAI.SeededTree.LiftCompatible.symm_apply line 627
  61. theorem OAI.SeededTree.LiftCompatible.insertion line 633
  62. def OAI.SeededTree.ordinaryGate line 642
  63. def OAI.SeededTree.ordinaryWord line 646
  64. theorem OAI.SeededTree.ordinaryWord_length line 648
  65. theorem OAI.SeededTree.circuit_ordinaryLift line 653
  66. theorem OAI.SeededTree.ordinaryLift_rootShift line 677
  67. theorem OAI.SeededTree.value_ordinaryWord line 690