OAI/Probability/ParisiFinite/RestrictLeft.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Restrict Left.

  1. def OAI.SKQAOA.restrictLeft line 17
  2. def OAI.SKQAOA.restrictRight line 20
  3. theorem OAI.SKQAOA.restrictLeft_append line 23
  4. theorem OAI.SKQAOA.restrictRight_append line 28
  5. theorem OAI.SKQAOA.overlapSum_split line 33
  6. def OAI.SKQAOA.blockCoeff line 39
  7. theorem OAI.SKQAOA.blockCoeff_increment line 42
  8. theorem OAI.SKQAOA.groundMaximum_eq_finiteMax line 58
  9. theorem OAI.SKQAOA.block_finiteMax line 66
  10. def OAI.SKQAOA.expectedMaximum line 90
  11. theorem OAI.SKQAOA.ground_integrable line 92
  12. theorem OAI.SKQAOA.expected_block_maximum line 97
  13. theorem OAI.SKQAOA.expectedMaximum_superadditive_pos line 116
  14. theorem OAI.SKQAOA.groundMaximum_zero line 123
  15. theorem OAI.SKQAOA.expectedMaximum_zero line 130
  16. theorem OAI.SKQAOA.expectedMaximum_superadditive line 133
  17. def OAI.SKQAOA.siteCoeff line 142
  18. theorem OAI.SKQAOA.site_increment line 144
  19. theorem OAI.SKQAOA.sk_to_site_increment line 155
  20. def OAI.SKQAOA.gaussianAbsoluteMean line 163
  21. theorem OAI.SKQAOA.integrable_abs_standard line 165
  22. theorem OAI.SKQAOA.site_maximum_le line 168
  23. theorem OAI.SKQAOA.expectedMaximum_le line 182
  24. theorem OAI.SKQAOA.tendsto_expectedGround line 202
  25. def OAI.TensorMatrix.lift line 231
  26. theorem OAI.TensorMatrix.lift_one line 235
  27. theorem OAI.TensorMatrix.lift_mul line 246
  28. def OAI.TensorMatrix.atSite line 254
  29. theorem OAI.TensorMatrix.local_one line 258
  30. theorem OAI.TensorMatrix.local_mul line 261
  31. theorem OAI.TensorMatrix.atSite_apply line 269
  32. theorem OAI.TensorMatrix.local_add line 281
  33. theorem OAI.TensorMatrix.local_zero line 288
  34. theorem OAI.TensorMatrix.local_smul line 293
  35. def OAI.TensorMatrix.localAlgHom line 300
  36. theorem OAI.TensorMatrix.local_exp line 310
  37. theorem OAI.TensorMatrix.atSite_commute line 315
  38. theorem OAI.TensorMatrix.exp_sum_atSite line 329
  39. theorem OAI.TensorMatrix.exp_sum_atSite_univ line 348
  40. def OAI.TwoState.swap line 356
  41. def OAI.TwoState.hadamard line 358
  42. def OAI.TwoState.hadamardUnit line 360
  43. theorem OAI.TwoState.conj_diagonal line 370
  44. theorem OAI.TwoState.exp_swap line 378
  45. def OAI.TwoState.rotation line 388
  46. theorem OAI.TwoState.rotation_eq_exp line 392
  47. theorem OAI.TwoState.rotation_apply line 406
  48. theorem OAI.SKQAOA.pauliX_eq_atSite line 414
  49. theorem OAI.SKQAOA.cost_evolution_eq_diagonal line 430
  50. theorem OAI.SKQAOA.mixer_evolution_eq_tensor line 439
  51. theorem OAI.SKQAOA.mixer_evolution_apply line 447
  52. def OAI.GaussianFourier.law line 461
  53. instance OAI.GaussianFourier.(instance at line 464) line 464
  54. theorem OAI.GaussianFourier.integral_exp line 469
  55. theorem OAI.GaussianFourier.integral_mul_exp line 473
  56. theorem OAI.GaussianFourier.integrable_exp line 485
  57. theorem OAI.GaussianFourier.integrable_mul_exp line 490
  58. theorem OAI.GaussianFourier.integral_exp_sum line 499
  59. theorem OAI.GaussianFourier.integrable_exp_sum line 507
  60. theorem OAI.GaussianFourier.coord_mul_exp_sum line 512
  61. theorem OAI.GaussianFourier.integrable_coord_exp_sum line 526
  62. theorem OAI.GaussianFourier.integral_coord_exp_sum line 538
  63. theorem OAI.TensorMatrix.lift_conjTranspose line 568
  64. theorem OAI.TensorMatrix.lift_diagonal line 574
  65. theorem OAI.TensorMatrix.local_diagonal line 586
  66. theorem OAI.TensorMatrix.conjugate_local line 604
  67. def OAI.TwoState.sign line 619
  68. def OAI.TwoState.z line 621
  69. def OAI.TwoState.y line 623
  70. theorem OAI.TwoState.z_apply line 625
  71. theorem OAI.TwoState.y_apply line 628
  72. theorem OAI.TwoState.rotation_star_mul line 631
  73. theorem OAI.TwoState.rotation_conjugate_z line 637
  74. def OAI.SKQAOA.pauliY line 652
  75. theorem OAI.SKQAOA.pauliZ_eq_atSite line 654
  76. theorem OAI.SKQAOA.mixer_conjugate_pauliZ line 661
  77. def OAI.SKQAOA.quad line 670
  78. theorem OAI.SKQAOA.quad_mulVec line 672
  79. theorem OAI.SKQAOA.quad_add line 677
  80. theorem OAI.SKQAOA.quad_smul line 681