OAI/Probability/ParisiFinite/WComm.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

W Comm.

  1. theorem OAI.CoherentFock.W_comm line 16
  2. theorem OAI.CoherentFock.W_centered_difference_le line 29
  3. theorem OAI.CoherentFock.W_fieldCoherent_sub_le line 54
  4. theorem OAI.CoherentFock.W_preField_sub_le line 84
  5. abbrev OAI.CoherentFock.SpinSpace line 109
  6. def OAI.CoherentFock.WZ line 113
  7. theorem OAI.CoherentFock.WZ_apply line 118
  8. theorem OAI.CoherentFock.norm_WZ line 121
  9. theorem OAI.CoherentFock.phase_neg_neg line 127
  10. theorem OAI.CoherentFock.WZ_zero line 130
  11. theorem OAI.CoherentFock.WZ_mul line 134
  12. theorem OAI.CoherentFock.exact_echo line 145
  13. theorem OAI.CoherentFock.exact_echo_unimodular line 154
  14. theorem OAI.CoherentFock.continuous_WZ line 159
  15. theorem OAI.CoherentFock.tendsto_WZ line 168
  16. theorem OAI.CoherentFock.WZ_error line 185
  17. theorem OAI.CoherentFock.corrected_echo line 190
  18. theorem OAI.CoherentFock.tendsto_corrected_echo line 204
  19. abbrev OAI.SpinOperators.Double line 227
  20. def OAI.SpinOperators.act line 230
  21. theorem OAI.SpinOperators.act_apply line 234
  22. theorem OAI.SpinOperators.act_one line 238
  23. theorem OAI.SpinOperators.act_mul line 242
  24. theorem OAI.SpinOperators.act_add line 249
  25. theorem OAI.SpinOperators.act_scalar line 254
  26. def OAI.SpinOperators.rep line 260
  27. theorem OAI.SpinOperators.rep_apply line 268
  28. theorem OAI.SpinOperators.act_adjoint line 273
  29. def OAI.SpinOperators.starRep line 282
  30. theorem OAI.SpinOperators.continuous_rep line 289
  31. theorem OAI.SpinOperators.act_exp line 295
  32. theorem OAI.SpinOperators.act_mem_unitary line 299
  33. theorem OAI.SpinOperators.norm_act line 303
  34. def OAI.WeightedMass.mass line 311
  35. theorem OAI.WeightedMass.nonneg line 313
  36. theorem OAI.WeightedMass.add_le line 316
  37. theorem OAI.WeightedMass.zero line 332
  38. theorem OAI.WeightedMass.smul line 334
  39. theorem OAI.WeightedMass.sum_le line 347
  40. theorem OAI.CoherentFock.secondTailBound_nonneg line 363
  41. theorem OAI.CoherentFock.secondTailBound_smul line 367
  42. theorem OAI.CoherentFock.secondTailBound_add line 372
  43. theorem OAI.CoherentFock.secondTailBound_sum line 377
  44. theorem OAI.CoherentFock.norm_preField_le line 382
  45. theorem OAI.CoherentFock.preField_add line 402
  46. theorem OAI.CoherentFock.preField_neg line 407
  47. theorem OAI.CoherentFock.preField_sub line 410
  48. abbrev OAI.CoherentFock.PreSpin line 414
  49. def OAI.CoherentFock.spinCoe line 416
  50. theorem OAI.CoherentFock.spinCoe_apply line 417
  51. def OAI.CoherentFock.preRoot line 419
  52. def OAI.CoherentFock.spinBound line 422
  53. def OAI.CoherentFock.matrixMass line 424
  54. theorem OAI.CoherentFock.spinBound_nonneg line 427
  55. theorem OAI.CoherentFock.secondTailBound_le_spinBound line 431
  56. theorem OAI.CoherentFock.spinBound_preRoot line 436
  57. theorem OAI.CoherentFock.spinCoe_preRoot line 453
  58. theorem OAI.CoherentFock.norm_spin_le_sum line 459
  59. def OAI.CoherentFock.spinField line 466
  60. theorem OAI.CoherentFock.spinField_apply line 468
  61. theorem OAI.CoherentFock.spinField_preRoot line 471
  62. theorem OAI.CoherentFock.WZ_spinField_sub_le line 476
  63. def OAI.CoherentFock.preZ line 495
  64. def OAI.CoherentFock.zField line 497
  65. theorem OAI.CoherentFock.zField_apply line 499
  66. theorem OAI.CoherentFock.spinBound_preZ line 505
  67. theorem OAI.CoherentFock.norm_spinField_le line 514
  68. theorem OAI.CoherentFock.norm_zField_le line 522
  69. theorem OAI.CoherentFock.zField_real_smul line 526
  70. theorem OAI.CoherentFock.zField_sub line 531
  71. theorem OAI.CoherentFock.WZ_taylor line 536
  72. def OAI.CoherentFock.probe line 549
  73. def OAI.CoherentFock.probeField line 552
  74. theorem OAI.CoherentFock.probe_apply line 555
  75. theorem OAI.CoherentFock.root_left_inverse line 558
  76. theorem OAI.CoherentFock.root_adjoint_unitary line 565
  77. theorem OAI.CoherentFock.norm_probe line 569
  78. theorem OAI.CoherentFock.probe_taylor line 573
  79. theorem OAI.CoherentFock.probeField_eq_spinField line 586
  80. theorem OAI.CoherentFock.probeField_real_smul line 590
  81. theorem OAI.CoherentFock.probeField_sub line 594
  82. theorem OAI.CoherentFock.norm_probeField_le line 598
  83. theorem OAI.CoherentFock.probe_cross line 605