OAI/Probability/ParisiFinite/PhysicalGate.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Physical Gate.

  1. def OAI.SKQAOA.physicalGate line 31
  2. def OAI.SKQAOA.physicalWord line 35
  3. def OAI.SKQAOA.gateGamma line 39
  4. def OAI.SKQAOA.gateBeta line 43
  5. def OAI.SKQAOA.wordGamma line 49
  6. def OAI.SKQAOA.wordBeta line 53
  7. theorem OAI.SKQAOA.physicalWord_nil line 57
  8. theorem OAI.SKQAOA.physicalWord_cons line 60
  9. theorem OAI.SKQAOA.physicalWord_eq_circuit line 65
  10. theorem OAI.SKQAOA.physicalWord_append line 73
  11. theorem OAI.SKQAOA.physicalGate_unitary line 80
  12. theorem OAI.SKQAOA.physicalWord_unitary line 86
  13. def OAI.SKQAOA.inverseGate line 92
  14. def OAI.SKQAOA.inverseWord line 96
  15. theorem OAI.SKQAOA.evolution_neg_adjoint line 99
  16. theorem OAI.SKQAOA.physicalGate_inverse line 107
  17. theorem OAI.SKQAOA.physicalWord_inverse line 113
  18. def OAI.SKQAOA.wordExpectedEnergy line 125
  19. theorem OAI.SKQAOA.wordExpectedEnergy_eq line 129
  20. theorem OAI.SKQAOA.finite_word_realizable line 136
  21. def OAI.SKQAOA.mixerPhase line 153
  22. theorem OAI.SKQAOA.star_mixerPhase_mul line 156
  23. theorem OAI.SKQAOA.mixer_evolution_plus line 170
  24. theorem OAI.SKQAOA.quad_phase line 186
  25. theorem OAI.SKQAOA.cost_evolution_preserves_quad line 192
  26. def OAI.SKQAOA.commutatorWord line 206
  27. theorem OAI.SKQAOA.commutator_quad line 211
  28. theorem OAI.SKQAOA.commutator_expectedEnergy line 223
  29. def OAI.SKQAOA.sizeCorrection line 238
  30. theorem OAI.SKQAOA.sizeCorrection_mem line 240
  31. theorem OAI.SKQAOA.commutator_scalar_remainder line 253
  32. theorem OAI.SKQAOA.commutator_uniform_energy_expansion line 296
  33. theorem OAI.SKQAOA.wordExpectedEnergy_costMixer line 312
  34. theorem OAI.SKQAOA.wordExpectedEnergy_cost_only line 322
  35. theorem OAI.SKQAOA.energy_only_not_a_congruence line 336
  36. theorem OAI.SKQAOA.quad_mixer_pair line 369
  37. theorem OAI.SKQAOA.quad_mixer_pair_interpolation line 401
  38. theorem OAI.SKQAOA.quad_mixer_cost_interpolation line 418
  39. theorem OAI.SKQAOA.integrable_word_energy line 430
  40. theorem OAI.SKQAOA.wordExpectedEnergy_mixer_interpolation line 437
  41. theorem OAI.SKQAOA.abs_wordExpectedEnergy_le line 473
  42. theorem OAI.SKQAOA.terminal_mixer_energy_lipschitz line 480
  43. def OAI.SKQAOA.Locality.IsSupported line 532
  44. theorem OAI.SKQAOA.Locality.IsSupported.mono line 537
  45. theorem OAI.SKQAOA.Locality.supported_zero line 541
  46. theorem OAI.SKQAOA.Locality.supported_one line 545
  47. theorem OAI.SKQAOA.Locality.IsSupported.add line 549
  48. theorem OAI.SKQAOA.Locality.IsSupported.mul line 554
  49. theorem OAI.SKQAOA.Locality.IsSupported.smul line 559
  50. theorem OAI.SKQAOA.Locality.supported_atSite line 563
  51. theorem OAI.SKQAOA.Locality.supported_pauliX line 570
  52. theorem OAI.SKQAOA.Locality.supported_pauliZ line 574
  53. theorem OAI.SKQAOA.Locality.pauliZ_hermitian line 578
  54. theorem OAI.SKQAOA.Locality.IsSupported.adjoint line 583
  55. theorem OAI.SKQAOA.Locality.IsSupported.exp line 591
  56. theorem OAI.SKQAOA.Locality.IsSupported.evolve line 595
  57. theorem OAI.SKQAOA.Locality.supported_finsetSum line 599
  58. theorem OAI.SKQAOA.Locality.commute_conjugate line 610
  59. theorem OAI.SKQAOA.Locality.IsSupported.mixer_conjugate line 625