OAI/Probability/ParisiFinite/PacketRegular.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Packet Regular.

  1. def OAI.PointedTree.PacketRegular line 22
  2. theorem OAI.PointedTree.PacketRegular.inner line 33
  3. theorem OAI.PointedTree.PacketRegular.zero line 60
  4. theorem OAI.PointedTree.PacketRegular.add line 69
  5. theorem OAI.PointedTree.PacketRegular.smul line 89
  6. theorem OAI.PointedTree.PacketRegular.neg line 102
  7. theorem OAI.PointedTree.PacketRegular.vac line 106
  8. theorem OAI.PointedTree.PacketRegular.root line 117
  9. theorem OAI.PointedTree.PacketRegular.cost line 148
  10. inductive OAI.PointedTree.ParamGate line 180
  11. def OAI.PointedTree.ParamGate.eval line 184
  12. def OAI.PointedTree.ParamGate.regular line 189
  13. def OAI.PointedTree.evalWord line 194
  14. theorem OAI.PointedTree.rootEquiv_symm_apply line 196
  15. theorem OAI.PointedTree.analyticAt_R line 201
  16. theorem OAI.PointedTree.ordinary_packetRegular line 211
  17. theorem OAI.PointedTree.ordinary_insertion_packetRegular line 265
  18. theorem OAI.CoherentFock.analyticAt_inner_spinPacket_creation line 281
  19. theorem OAI.PointedTree.PacketRegular.inner_creation line 308
  20. theorem OAI.PointedTree.analyticAt_ordinary_insertion_gram line 321
  21. theorem OAI.PointedTree.analyticAt_ordinaryValue line 330
  22. theorem OAI.AnalyticVisibility.dense_nonzero line 352
  23. theorem OAI.AnalyticVisibility.dense_all_nonzero line 371
  24. theorem OAI.AnalyticVisibility.exists_perturbation line 392
  25. def OAI.HilbertChain.up line 412
  26. theorem OAI.HilbertChain.up_self line 415
  27. theorem OAI.HilbertChain.up_succ line 418
  28. theorem OAI.HilbertChain.up_comp line 422
  29. instance OAI.HilbertChain.(instance at line 429) line 429
  30. abbrev OAI.HilbertChain.Algebraic line 435
  31. def OAI.HilbertChain.incl line 437
  32. theorem OAI.HilbertChain.incl_up line 440
  33. def OAI.HilbertChain.inner line 443
  34. theorem OAI.HilbertChain.inner_incl line 447
  35. theorem OAI.HilbertChain.induction line 451
  36. theorem OAI.HilbertChain.induction₂ line 454
  37. theorem OAI.HilbertChain.induction₃ line 458
  38. def OAI.HilbertChain.core line 463
  39. instance OAI.HilbertChain.(instance at line 473) line 473
  40. instance OAI.HilbertChain.(instance at line 475) line 475
  41. theorem OAI.HilbertChain.inner_incl' line 478
  42. def OAI.HilbertChain.inclusion line 481
  43. abbrev OAI.HilbertChain.Space line 484
  44. def OAI.HilbertChain.embed line 486
  45. theorem OAI.HilbertChain.embed_up line 489
  46. theorem OAI.HilbertChain.embed_step line 495
  47. theorem OAI.HilbertChain.denseRange_embed line 507
  48. theorem OAI.HilbertChain.lift_compat line 526
  49. def OAI.HilbertChain.liftAlgebraic line 535
  50. theorem OAI.HilbertChain.liftAlgebraic_incl line 545
  51. def OAI.HilbertChain.lift line 558
  52. theorem OAI.HilbertChain.lift_embed line 569
  53. theorem OAI.HilbertChain.ext line 579
  54. abbrev OAI.PointedTree.ModeSpace line 591
  55. abbrev OAI.PointedTree.wholeStep line 593
  56. abbrev OAI.PointedTree.modeStep line 594
  57. abbrev OAI.PointedTree.WholeInfinity line 595
  58. abbrev OAI.PointedTree.ModeInfinity line 596
  59. abbrev OAI.PointedTree.wholeEmbed line 597
  60. abbrev OAI.PointedTree.modeEmbed line 598
  61. def OAI.PointedTree.vacuumInfinity line 600
  62. theorem OAI.PointedTree.embed_vac line 602
  63. theorem OAI.PointedTree.norm_vacuumInfinity line 607
  64. def OAI.PointedTree.modeInWhole line 611
  65. theorem OAI.PointedTree.modeInWhole_embed line 618
  66. theorem OAI.PointedTree.modeInWhole_centered line 623
  67. def OAI.PointedTree.shiftInfinity line 634
  68. theorem OAI.PointedTree.shiftInfinity_embed line 642
  69. def OAI.PointedTree.energyInfinity line 647
  70. theorem OAI.PointedTree.energyInfinity_embed line 649
  71. theorem OAI.PointedTree.continuous_energyInfinity line 657
  72. theorem OAI.PointedTree.energyInfinity_sub_le line 661
  73. def OAI.PointedTree.insertionInfinity line 678
  74. theorem OAI.PointedTree.insertionInfinity_stable line 681
  75. theorem OAI.PointedTree.norm_insertionInfinity line 689
  76. theorem OAI.PointedTree.energy_insertionInfinity line 692