OAI/Probability/ParisiFinite/SpinFlip.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Spin Flip.

  1. def OAI.SKQAOA.Masks.spinFlip line 47
  2. def OAI.SKQAOA.Masks.flipGate line 53
  3. theorem OAI.SKQAOA.Masks.spinFlip_symm line 56
  4. theorem OAI.SKQAOA.Masks.flipGate_adjoint line 60
  5. theorem OAI.SKQAOA.Masks.flipGate_square line 66
  6. theorem OAI.SKQAOA.Masks.flipGate_unitary line 72
  7. theorem OAI.SKQAOA.Masks.spin_spinFlip line 77
  8. theorem OAI.SKQAOA.Masks.flipGate_conjugate_cost line 84
  9. theorem OAI.MaskSign.pair_projection line 122
  10. def OAI.SKQAOA.Masks.pairEdges line 149
  11. theorem OAI.SKQAOA.Masks.pairCost_identity line 154
  12. theorem OAI.SKQAOA.Masks.pairEdges_distinct line 179
  13. def OAI.SKQAOA.Masks.signReal line 194
  14. theorem OAI.SKQAOA.Masks.signReal_cast line 197
  15. def OAI.SKQAOA.Masks.signedDisorder line 201
  16. theorem OAI.SKQAOA.Masks.flipGate_cost line 205
  17. def OAI.SKQAOA.Masks.pairWeight line 210
  18. theorem OAI.SKQAOA.Masks.pairCost_weighted line 213
  19. theorem OAI.SKQAOA.Masks.flipGate_evolution line 226
  20. theorem OAI.SKQAOA.Masks.evolution_list_sum line 241
  21. theorem OAI.SKQAOA.Masks.pairCost_evolution_word line 262
  22. theorem OAI.SKQAOA.Masks.flipGate_tensor line 298
  23. theorem OAI.SKQAOA.Masks.tensor_scalar line 312
  24. def OAI.SKQAOA.Masks.maskedMixer line 318
  25. theorem OAI.SKQAOA.Masks.maskedMixer_evolution line 322
  26. theorem OAI.SKQAOA.Masks.maskedMixer_flip line 341
  27. theorem OAI.SKQAOA.Helpers.twoState_ZY line 362
  28. theorem OAI.SKQAOA.Helpers.pauli_ZY line 368
  29. theorem OAI.SKQAOA.Helpers.commute_pauliX line 376
  30. theorem OAI.SKQAOA.Helpers.disjoint_ne line 382
  31. theorem OAI.SKQAOA.Helpers.coefficient_bracket line 389
  32. theorem OAI.SKQAOA.Helpers.pivot_sum_commutator line 398
  33. def OAI.SKQAOA.Helpers.b line 420
  34. def OAI.SKQAOA.Helpers.B line 424
  35. def OAI.SKQAOA.Helpers.F line 428
  36. theorem OAI.SKQAOA.Helpers.b_commute_local line 432
  37. theorem OAI.SKQAOA.Helpers.B_commute_local line 439
  38. theorem OAI.SKQAOA.Helpers.F_commute_local line 450
  39. theorem OAI.SKQAOA.Helpers.B_commute_F line 459
  40. theorem OAI.SKQAOA.Helpers.helper_commutator line 474
  41. theorem OAI.SKQAOA.Masks.maskedMixer_hermitian line 502
  42. theorem OAI.SKQAOA.Masks.maskedMixer_conjugate line 515
  43. theorem OAI.SKQAOA.Masks.pairCost_physical_word line 530
  44. theorem OAI.SKQAOA.Helpers.pauliX_square line 552
  45. theorem OAI.SKQAOA.Helpers.BF_expansion line 559
  46. theorem OAI.SKQAOA.Helpers.diagonal_sender line 574
  47. def OAI.SKQAOA.Helpers.diagonalGenerator line 588
  48. theorem OAI.SKQAOA.Helpers.diagonalGenerator_pinned line 594
  49. theorem OAI.SKQAOA.Helpers.preserve_pin line 611