OAI/Probability/ParisiFinite/InsertionFromForward.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Insertion From Forward.

  1. theorem OAI.ForwardControl.insertion_from_forward line 21
  2. theorem OAI.ForwardControl.insertion_split_bound line 35
  3. theorem OAI.ForwardControl.selective_flip_bound line 59
  4. theorem OAI.ForwardControl.actual_flip_change line 79
  5. theorem OAI.ForwardControl.special_transport_bound line 96
  6. theorem OAI.PointedTree.abs_treeEnergy_le line 112
  7. def OAI.PointedTree.ordinaryValue line 120
  8. theorem OAI.PointedTree.ordinary_energy_succ line 122
  9. theorem OAI.PointedTree.ordinary_energy_stable line 126
  10. theorem OAI.PointedTree.abs_ordinaryValue_le_one line 132
  11. theorem OAI.SpinOperators.actEquiv_symm_apply line 139
  12. theorem OAI.CoherentFock.rootY_apply line 156
  13. theorem OAI.CoherentFock.WZ_rootY line 160
  14. theorem OAI.CoherentFock.WZ_same line 165
  15. theorem OAI.CoherentFock.one_layer_insertion line 174
  16. def OAI.PointedTree.initialDirection line 201
  17. theorem OAI.PointedTree.initialDirection_coe line 203
  18. theorem OAI.PointedTree.initialDirection_norm line 206
  19. theorem OAI.PointedTree.initialDirection_empty line 209
  20. theorem OAI.PointedTree.ordinary_one_insertion line 215
  21. def OAI.PointedTree.initializationWord line 231
  22. theorem OAI.PointedTree.initialization_op line 234
  23. theorem OAI.CoherentFock.W_vacuum line 248
  24. theorem OAI.CoherentFock.kernel_zero_left line 249
  25. theorem OAI.PointedTree.inv_sqrt_two_sq line 257
  26. def OAI.PointedTree.spinPair line 261
  27. theorem OAI.PointedTree.spinPair_zero line 264
  28. theorem OAI.PointedTree.spinPair_one line 265
  29. theorem OAI.PointedTree.inner_spinPair line 267
  30. def OAI.PointedTree.spinCoefficient line 272
  31. theorem OAI.PointedTree.spinCoefficient_conj line 273
  32. theorem OAI.PointedTree.spinCoefficient_sq line 275
  33. theorem OAI.PointedTree.plusEmbedding_pair line 277
  34. theorem OAI.PointedTree.rootZ_vac_pair line 282
  35. theorem OAI.PointedTree.rootY_WZ_vac_pair line 287
  36. theorem OAI.PointedTree.inner_rootZ_vac_creation line 292
  37. theorem OAI.PointedTree.inner_rootZ_vac_rootY_WZ line 297
  38. theorem OAI.PointedTree.inner_rootY_WZ_creation line 305
  39. def OAI.PointedTree.highDirection line 321
  40. theorem OAI.PointedTree.highDirection_coe line 324
  41. theorem OAI.PointedTree.highDirection_norm line 339
  42. theorem OAI.PointedTree.highDirection_empty line 342
  43. theorem OAI.PointedTree.initial_inner_highDirection line 356
  44. theorem OAI.PointedTree.ordinary_one_mode line 375
  45. theorem OAI.PointedTree.inner_highDirection_creation line 391
  46. theorem OAI.PointedTree.inner_initial_rootShift line 409
  47. theorem OAI.PointedTree.inner_highDirection_rootShift line 415
  48. theorem OAI.PointedTree.inner_initialDirection_self line 420
  49. theorem OAI.PointedTree.treeEnergy_one line 427
  50. theorem OAI.PointedTree.ordinaryValue_one line 446
  51. def OAI.SeedInitialization.amplitude line 456
  52. def OAI.SeedInitialization.delta line 457
  53. def OAI.SeedInitialization.gamma line 458
  54. theorem OAI.SeedInitialization.amplitude_pos line 460
  55. theorem OAI.SeedInitialization.amplitude_le_one line 462
  56. theorem OAI.SeedInitialization.sin_delta line 465
  57. theorem OAI.SeedInitialization.cos_delta line 468
  58. theorem OAI.SeedInitialization.cos_two_delta line 471
  59. theorem OAI.SeedInitialization.sin_two_delta line 478
  60. theorem OAI.SeedInitialization.gamma_cos_error line 482
  61. theorem OAI.SeedInitialization.gamma_sin line 489
  62. theorem OAI.SeedInitialization.tendsto_amplitude line 496
  63. theorem OAI.SeedInitialization.tendsto_delta line 498
  64. theorem OAI.SeedInitialization.tendsto_cos_delta line 502
  65. theorem OAI.SeedInitialization.tendsto_cos_two_delta line 505
  66. theorem OAI.SeedInitialization.tendsto_sin_two_delta line 508
  67. theorem OAI.SeedInitialization.tendsto_gamma_cos_error line 511
  68. theorem OAI.SeedInitialization.tendsto_gamma_sin line 518
  69. theorem OAI.SeedInitialization.tendsto_gamma line 525
  70. theorem OAI.SeedInitialization.tendsto_gamma_sq_exp line 528
  71. def OAI.SeedInitialization.phaseAngle line 540
  72. theorem OAI.SeedInitialization.tendsto_phaseAngle line 543
  73. theorem OAI.UnitarySplit.inverse line 556
  74. def OAI.SeedInitialization.initialMap line 576
  75. def OAI.SeedInitialization.ordinaryMap line 580
  76. def OAI.SeedInitialization.specialMap line 583
  77. def OAI.SeedInitialization.ordinaryCoefficient line 587
  78. def OAI.SeedInitialization.specialCoefficient line 589
  79. def OAI.SeedInitialization.specialPhase line 591
  80. theorem OAI.SeedInitialization.initialMap_apply line 594
  81. theorem OAI.SeedInitialization.ordinaryMap_apply line 597
  82. theorem OAI.SeedInitialization.specialMap_apply line 599
  83. theorem OAI.SeedInitialization.exact_split line 604
  84. theorem OAI.SeedInitialization.norm_specialPhase line 617
  85. theorem OAI.SeedInitialization.norm_special_component line 620
  86. def OAI.SeedInitialization.address line 628
  87. theorem OAI.SeedInitialization.norm_address line 632
  88. theorem OAI.SeedInitialization.address_exact_normalization line 638
  89. theorem OAI.RootSpin.Y_mul_X line 652
  90. theorem OAI.RootSpin.R_quarter_conjugate_Z line 656