OAI/Probability/ParisiFinite/CostState.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Cost State.

  1. def OAI.SKQAOA.costState line 16
  2. theorem OAI.SKQAOA.costState_apply line 19
  3. theorem OAI.SKQAOA.plus_squared line 24
  4. def OAI.SKQAOA.phaseCoeff line 31
  5. theorem OAI.SKQAOA.phase_sum line 34
  6. theorem OAI.SKQAOA.costState_pair line 43
  7. theorem OAI.SKQAOA.integrable_coord_costState_pair line 64
  8. theorem OAI.SKQAOA.integral_coord_costState_pair line 76
  9. def OAI.SKQAOA.flipAt line 97
  10. theorem OAI.SKQAOA.flipAt_self line 100
  11. theorem OAI.SKQAOA.flipAt_ne line 103
  12. theorem OAI.SKQAOA.spin_flipAt_self line 106
  13. theorem OAI.SKQAOA.spin_flipAt_ne line 110
  14. theorem OAI.SKQAOA.pauliZ_mulVec line 113
  15. theorem OAI.SKQAOA.pauliX_mulVec line 117
  16. theorem OAI.SKQAOA.pauliY_eq line 131
  17. theorem OAI.SKQAOA.pauliY_mulVec line 136
  18. theorem OAI.SKQAOA.overlapSum_flipAt line 143
  19. theorem OAI.SKQAOA.phaseCoeff_flip_edge_left line 162
  20. theorem OAI.SKQAOA.phaseCoeff_flip_edge_right line 171
  21. theorem OAI.SKQAOA.phaseCoeff_self line 180
  22. theorem OAI.SKQAOA.phaseCoeff_flip_both line 183
  23. theorem OAI.SKQAOA.phaseCoeff_square_sum_flip line 191
  24. theorem OAI.SKQAOA.integrable_coord_quad_transition line 215
  25. theorem OAI.SKQAOA.integral_coord_quad_transition line 232
  26. theorem OAI.SKQAOA.integral_coord_ZZ line 251
  27. theorem OAI.SKQAOA.integral_coord_YY line 262
  28. theorem OAI.SKQAOA.sum_configuration_normalized line 278
  29. theorem OAI.SKQAOA.integral_coord_YZ line 284
  30. theorem OAI.SKQAOA.integral_coord_ZY line 313
  31. theorem OAI.SKQAOA.integrable_coord_quad line 345
  32. theorem OAI.SKQAOA.qaoaState_one line 361
  33. theorem OAI.SKQAOA.conjugate_mul line 365
  34. theorem OAI.SKQAOA.quad_qaoaState_one_edge line 372
  35. theorem OAI.SKQAOA.integrable_coord_qaoaState_one_edge line 386
  36. theorem OAI.SKQAOA.integral_coord_qaoaState_one_edge line 400
  37. theorem OAI.SKQAOA.quad_finsetSum line 437
  38. theorem OAI.SKQAOA.quad_cost line 445
  39. theorem OAI.SKQAOA.integrable_quad_cost_one line 450
  40. theorem OAI.SKQAOA.integral_quad_cost_one line 455
  41. theorem OAI.SKQAOA.card_edges_real line 465
  42. theorem OAI.SKQAOA.expectedEnergy_one line 472
  43. theorem OAI.SKQAOA.tendsto_sizeCorrection line 498
  44. theorem OAI.SKQAOA.tendsto_expectedEnergy_one line 508
  45. theorem OAI.SKQAOA.value_one line 521
  46. theorem OAI.SKQAOA.explicit_one_layer_value line 526
  47. theorem OAI.SKGaussian.expected_field_logPartition_le_of_orthogonal line 539
  48. theorem OAI.SKGaussian.expected_field_logPartition_le line 553
  49. def OAI.SKQAOA.pressure line 573
  50. def OAI.SKQAOA.freeEnergy line 576
  51. def OAI.SKQAOA.limitingFreeEnergy line 578
  52. theorem OAI.SKQAOA.field_scale line 580
  53. theorem OAI.SKQAOA.scaled_increment line 585
  54. theorem OAI.SKQAOA.field_skCoeff line 590
  55. theorem OAI.SKQAOA.pressure_integrable line 593
  56. theorem OAI.SKQAOA.block_partition line 600
  57. theorem OAI.SKQAOA.block_logPartition line 620
  58. theorem OAI.SKQAOA.expected_block_logPartition line 627
  59. theorem OAI.SKQAOA.pressure_superadditive_pos line 646
  60. theorem OAI.SKQAOA.pressure_zero line 659
  61. theorem OAI.SKQAOA.pressure_superadditive line 662