OAI/Probability/ParisiFinite/SpinCoeAdd.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

Spin Coe Add.

  1. theorem OAI.CoherentFock.spinCoe_add line 39
  2. theorem OAI.CoherentFock.spinCoe_zero line 43
  3. theorem OAI.CoherentFock.spinMass_add line 48
  4. def OAI.CoherentFock.preSpinW line 53
  5. theorem OAI.CoherentFock.spinCoe_preSpinW line 55
  6. theorem OAI.CoherentFock.spinMass_preSpinW line 60
  7. theorem OAI.CoherentFock.SpinRadiusLE.preSpinW line 63
  8. theorem OAI.CoherentFock.BoundedPacket.zero line 68
  9. theorem OAI.CoherentFock.BoundedPacket.add line 72
  10. theorem OAI.CoherentFock.BoundedPacket.sum line 82
  11. theorem OAI.CoherentFock.BoundedPacket.weyl line 91
  12. def OAI.CoherentFock.spinSector line 110
  13. def OAI.CoherentFock.projectSpin line 112
  14. def OAI.CoherentFock.signedMode line 113
  15. theorem OAI.CoherentFock.projectSpin_apply line 115
  16. theorem OAI.CoherentFock.projectSpin_sum line 120
  17. theorem OAI.CoherentFock.spinW_project line 125
  18. theorem OAI.CoherentFock.projectSpin_projectSpin line 128
  19. theorem OAI.CoherentFock.norm_signedMode line 135
  20. theorem OAI.CoherentFock.WZ_project line 139
  21. theorem OAI.CoherentFock.spinW_mul_apply line 147
  22. theorem OAI.CoherentFock.spinW_add_split line 153
  23. theorem OAI.CoherentFock.signedMode_add line 159
  24. theorem OAI.CoherentFock.WZ_sector_split line 164
  25. theorem OAI.CoherentFock.rotated_WZ_sector_split line 174
  26. theorem OAI.CoherentFock.BoundedPacket.project line 189
  27. theorem OAI.CoherentFock.BoundedPacket.rotated_sector_tail line 192
  28. theorem OAI.CoherentFock.projectSpin_spinW line 211
  29. theorem OAI.CoherentFock.WZ_on_sector line 214
  30. theorem OAI.CoherentFock.WZ_packet_bounded line 221
  31. theorem OAI.CoherentFock.WZ_packet_shift line 232
  32. theorem OAI.CoherentFock.rootX_sector line 237
  33. theorem OAI.CoherentFock.halfMixer_sector line 244
  34. theorem OAI.CoherentFock.BoundedPacket.finite_uniform line 257
  35. theorem OAI.CoherentFock.BoundedPacket.cost_packet_tail line 271
  36. theorem OAI.CoherentFock.low_insertion_scaled_bound line 291
  37. theorem OAI.CoherentFock.low_insertion_tendsto line 325
  38. def OAI.SeedInitialization.eInfinity line 359
  39. def OAI.SeedInitialization.vInfinity line 360
  40. def OAI.SeedInitialization.highInfinity line 362
  41. def OAI.SeedInitialization.dInfinity line 363
  42. def OAI.SeedInitialization.wordInfinity line 364
  43. theorem OAI.SeedInitialization.norm_eInfinity line 367
  44. theorem OAI.SeedInitialization.norm_vInfinity line 368
  45. theorem OAI.SeedInitialization.norm_highInfinity line 369
  46. theorem OAI.SeedInitialization.embed_initialDirection line 372
  47. theorem OAI.SeedInitialization.vInfinity_embed line 375
  48. theorem OAI.SeedInitialization.vInfinity_eq line 379
  49. theorem OAI.SeedInitialization.modeFock_eInfinity line 385
  50. theorem OAI.SeedInitialization.spinMap_vacuum line 390
  51. theorem OAI.SeedInitialization.modeFock_highInfinity line 397
  52. theorem OAI.SeedInitialization.initialMap_apply_complex line 413
  53. theorem OAI.SeedInitialization.ordinaryLocal_initialization line 419
  54. theorem OAI.SeedInitialization.dInfinity_embed line 426
  55. theorem OAI.SeedInitialization.dInfinity_bounded line 431
  56. theorem OAI.SeedInitialization.dInfinity_approx_high line 435
  57. def OAI.SeedInitialization.lowInfinity line 445
  58. theorem OAI.SeedInitialization.lowInfinity_apply line 449
  59. def OAI.SeedInitialization.phaseInfinity line 453
  60. def OAI.SeedInitialization.ordinaryPartInfinity line 456
  61. def OAI.SeedInitialization.specialPartInfinity line 460
  62. theorem OAI.SeedInitialization.ordinaryPartInfinity_apply line 464
  63. theorem OAI.SeedInitialization.specialPartInfinity_apply line 468
  64. theorem OAI.SeedInitialization.norm_phaseInfinity line 472
  65. theorem OAI.SeedInitialization.exact_splitInfinity line 474
  66. theorem OAI.SeedInitialization.norm_specialPartInfinity line 479
  67. theorem OAI.SeedInitialization.lowInfinity_accuracy line 484
  68. theorem OAI.SeedInitialization.highInfinity_escapes line 509
  69. theorem OAI.SeedInitialization.signedMode_smul line 530
  70. theorem OAI.SeedInitialization.specialCoefficient_eq line 535
  71. theorem OAI.SeedInitialization.special_displacement line 540
  72. theorem OAI.SeedInitialization.specialPart_expanded line 546
  73. def OAI.SeedInitialization.initialCenter line 556
  74. def OAI.SeedInitialization.initialTail line 559
  75. theorem OAI.SeedInitialization.initialCenter_scale line 565
  76. theorem OAI.SeedInitialization.initial_special_packets line 572
  77. theorem OAI.SeedInitialization.initialTail_bounded line 585
  78. theorem OAI.SeedInitialization.initialTail_sector line 594
  79. theorem OAI.SeedInitialization.norm_initialCenter line 598
  80. def OAI.CoherentFock.PacketExpansion line 615
  81. theorem OAI.CoherentFock.PacketExpansion.close line 625
  82. theorem OAI.CoherentFock.PacketExpansion.bounded_cost line 637
  83. theorem OAI.CoherentFock.PacketExpansion.huge_cost line 657
  84. theorem OAI.CoherentFock.PacketExpansion.half_mixer line 677