OAI/Probability/ParisiFinite/TendstoDyadicRound.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Tendsto Dyadic Round.

  1. lemma OAI.BrownianConstruction.tendsto_dyadicRound line 18
  2. lemma OAI.BrownianConstruction.preBrownian_tendstoInMeasure line 32
  3. def OAI.BrownianConstruction.continuousModification line 65
  4. lemma OAI.BrownianConstruction.continuousModification_ae_continuous line 68
  5. lemma OAI.BrownianConstruction.continuousModification_ae_eq line 73
  6. lemma OAI.BrownianConstruction.continuousModification_isBrownian line 82
  7. abbrev OAI.BrownianConstruction.BrownianHilbert line 97
  8. def OAI.BrownianConstruction.brownianBasisIndex line 98
  9. def OAI.BrownianConstruction.brownianBasis line 99
  10. abbrev OAI.BrownianConstruction.BrownianSample line 101
  11. def OAI.BrownianConstruction.brownianMeasure line 102
  12. instance OAI.BrownianConstruction.brownianMeasure_probability line 103
  13. def OAI.BrownianConstruction.brownianMotion line 106
  14. theorem OAI.BrownianConstruction.brownianMotion_isBrownian line 108
  15. abbrev OAI.SKQAOA.Configuration line 124
  16. abbrev OAI.SKQAOA.Edge line 127
  17. abbrev OAI.SKQAOA.Disorder line 129
  18. abbrev OAI.SKQAOA.State line 130
  19. abbrev OAI.SKQAOA.Operator line 131
  20. def OAI.SKQAOA.disorderLaw line 134
  21. def OAI.SKQAOA.spin line 137
  22. def OAI.SKQAOA.hamiltonian line 141
  23. def OAI.SKQAOA.pauliZ line 145
  24. def OAI.SKQAOA.pauliX line 149
  25. def OAI.SKQAOA.cost line 153
  26. def OAI.SKQAOA.mixer line 157
  27. def OAI.SKQAOA.plus line 160
  28. def OAI.SKQAOA.evolution line 164
  29. def OAI.SKQAOA.circuit line 168
  30. def OAI.SKQAOA.qaoaState line 176
  31. def OAI.SKQAOA.energyDensity line 180
  32. def OAI.SKQAOA.expectedEnergy line 185
  33. def OAI.SKQAOA.groundMaximum line 189
  34. def OAI.SKQAOA.expectedGround line 192
  35. def OAI.SKQAOA.Pstar line 196
  36. def OAI.SKQAOA.value line 199
  37. def OAI.SKQAOA.Q line 202
  38. theorem OAI.SKQAOA.cost_eq_diagonal line 206
  39. theorem OAI.SKQAOA.flip_flip line 218
  40. theorem OAI.SKQAOA.flip_eq_iff line 227
  41. theorem OAI.SKQAOA.cost_hermitian line 232
  42. theorem OAI.SKQAOA.pauliX_hermitian line 241
  43. theorem OAI.SKQAOA.mixer_hermitian line 246
  44. theorem OAI.SKQAOA.evolution_zero line 251
  45. theorem OAI.SKQAOA.evolution_unitary line 256
  46. theorem OAI.SKQAOA.circuit_unitary line 272
  47. def OAI.SKQAOA.mass line 284
  48. theorem OAI.SKQAOA.mass_eq_dot line 286
  49. theorem OAI.SKQAOA.unitary_preserves_mass line 290
  50. theorem OAI.SKQAOA.plus_mass line 300
  51. theorem OAI.SKQAOA.qaoaState_mass line 309
  52. theorem OAI.SKQAOA.energyDensity_eq line 315
  53. theorem OAI.SKQAOA.hamiltonian_le_groundMaximum line 330
  54. theorem OAI.SKQAOA.energyDensity_le_groundMaximum line 335
  55. theorem OAI.SKQAOA.spin_abs line 350
  56. def OAI.SKQAOA.couplingEnvelope line 356
  57. theorem OAI.SKQAOA.couplingEnvelope_nonneg line 359
  58. theorem OAI.SKQAOA.hamiltonian_abs_le line 364
  59. theorem OAI.SKQAOA.groundMaximum_abs_le line 375
  60. theorem OAI.SKQAOA.energyDensity_abs_le line 385
  61. theorem OAI.SKQAOA.hamiltonian_continuous line 406
  62. theorem OAI.SKQAOA.cost_evolution_continuous line 411
  63. theorem OAI.SKQAOA.circuit_continuous line 420
  64. theorem OAI.SKQAOA.qaoaState_continuous line 428
  65. theorem OAI.SKQAOA.energyDensity_continuous line 432
  66. theorem OAI.SKQAOA.groundMaximum_continuous line 442
  67. theorem OAI.SKQAOA.coupling_integrable line 451
  68. theorem OAI.SKQAOA.couplingEnvelope_integrable line 458
  69. theorem OAI.SKQAOA.groundMaximum_integrable line 463
  70. theorem OAI.SKQAOA.energyDensity_integrable line 470
  71. theorem OAI.SKQAOA.expectedEnergy_le_expectedGround line 479
  72. theorem OAI.SKQAOA.circuit_pad line 488
  73. theorem OAI.SKQAOA.expectedEnergy_pad line 493
  74. theorem OAI.SKQAOA.value_pad line 498
  75. theorem OAI.SKQAOA.spin_sq line 503
  76. theorem OAI.SKQAOA.sum_symmetric_pairs line 509
  77. def OAI.SKQAOA.skCoeff line 546
  78. theorem OAI.SKQAOA.hamiltonian_eq_coeff line 549
  79. def OAI.SKQAOA.overlapSum line 557
  80. theorem OAI.SKQAOA.edge_overlap line 560
  81. theorem OAI.SKQAOA.overlapSum_self line 578
  82. theorem OAI.SKQAOA.coeff_covariance line 582
  83. theorem OAI.SKQAOA.coeff_increment line 601