OAI/Probability/ParisiFinite/MaskedDisorder.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Masked Disorder.

  1. def OAI.SKQAOA.Locality.maskedDisorder line 33
  2. def OAI.SKQAOA.Locality.maskedCost line 36
  3. theorem OAI.SKQAOA.Locality.maskedCost_univ line 39
  4. theorem OAI.SKQAOA.Locality.maskedCost_empty line 45
  5. theorem OAI.SKQAOA.Locality.maskedCost_sum line 48
  6. theorem OAI.SKQAOA.Locality.maskedCost_hermitian line 53
  7. theorem OAI.SKQAOA.Locality.maskedCost_commute line 56
  8. def OAI.SKQAOA.Locality.touches line 61
  9. instance OAI.SKQAOA.Locality.(instance at line 63) line 63
  10. def OAI.SKQAOA.Locality.activeEdges line 66
  11. def OAI.SKQAOA.Locality.inactiveEdges line 69
  12. def OAI.SKQAOA.Locality.neighborhood line 72
  13. theorem OAI.SKQAOA.Locality.subset_neighborhood line 75
  14. theorem OAI.SKQAOA.Locality.active_endpoints line 78
  15. theorem OAI.SKQAOA.Locality.maskedCost_active_supported line 84
  16. theorem OAI.SKQAOA.Locality.commute_maskedCost_inactive line 93
  17. theorem OAI.SKQAOA.Locality.maskedCost_split line 104
  18. theorem OAI.SKQAOA.Locality.evolution_add_of_commute line 111
  19. theorem OAI.SKQAOA.Locality.unitary_conjugate_eq_self line 117
  20. theorem OAI.SKQAOA.Locality.cost_conjugate_local line 124
  21. theorem OAI.SKQAOA.Locality.IsSupported.cost_conjugate line 143
  22. theorem OAI.SKQAOA.Locality.activeEdges_mono line 163
  23. theorem OAI.SKQAOA.Locality.neighborhood_mono line 170
  24. def OAI.SKQAOA.Locality.relevantEdges line 179
  25. theorem OAI.SKQAOA.Locality.relevantEdges_subset line 185
  26. theorem OAI.SKQAOA.Locality.relevantEdges_mono line 194
  27. def OAI.SKQAOA.Locality.wordConjugate line 207
  28. theorem OAI.SKQAOA.Locality.wordConjugate_nil line 211
  29. theorem OAI.SKQAOA.Locality.wordConjugate_cons line 214
  30. theorem OAI.SKQAOA.Locality.wordConjugate_cost line 221
  31. theorem OAI.SKQAOA.Locality.wordConjugate_mixer line 227
  32. theorem OAI.SKQAOA.Locality.wordConjugate_eq_of_relevant_subset line 234
  33. theorem OAI.SKQAOA.Locality.wordConjugate_insert_irrelevant line 264
  34. def OAI.FiniteEdgeExpansion.mixedDifference line 288
  35. theorem OAI.FiniteEdgeExpansion.mixedDifference_empty line 291
  36. theorem OAI.FiniteEdgeExpansion.mixedDifference_insert line 296
  37. theorem OAI.FiniteEdgeExpansion.mixedDifference_eq_zero_of_irrelevant line 328
  38. theorem OAI.FiniteEdgeExpansion.reconstruction line 342
  39. def OAI.FiniteEdgeExpansion.partition line 361
  40. def OAI.FiniteEdgeExpansion.coefficient line 364
  41. theorem OAI.FiniteEdgeExpansion.partition_expansion line 370
  42. theorem OAI.FiniteEdgeExpansion.coefficient_eq_mixedDifference line 381
  43. theorem OAI.FiniteEdgeExpansion.coefficient_eq_zero_of_irrelevant line 395
  44. def OAI.SKQAOA.Locality.annealedObservable line 414
  45. theorem OAI.SKQAOA.Locality.annealed_mixedDifference_eq_zero line 421
  46. def OAI.SKQAOA.Locality.averagedMarkedWord line 442
  47. theorem OAI.SKQAOA.Locality.marked_cluster_eq_zero line 449
  48. def OAI.SKQAOA.qaoaWord line 468
  49. theorem OAI.SKQAOA.physicalWord_qaoaWord line 473
  50. instance OAI.SKQAOA.SiteHistories.bitsInhabited line 481
  51. def OAI.SKQAOA.SiteHistories.maskPhase line 485
  52. lemma OAI.SKQAOA.SiteHistories.masked_phase_sum line 489
  53. lemma OAI.SKQAOA.SiteHistories.coord_masked_history line 498
  54. lemma OAI.SKQAOA.SiteHistories.integral_coord_masked line 512
  55. lemma OAI.SKQAOA.SiteHistories.integrable_coord_masked line 533
  56. lemma OAI.SKQAOA.SiteHistories.quad_ZZ line 542
  57. theorem OAI.SKQAOA.SiteHistories.averagedMarkedWord_history line 552
  58. def OAI.SKQAOA.SiteHistories.rootFactor line 601
  59. def OAI.SKQAOA.SiteHistories.factor line 607
  60. def OAI.SKQAOA.SiteHistories.partition line 611
  61. def OAI.SKQAOA.SiteHistories.cluster line 614
  62. lemma OAI.SKQAOA.SiteHistories.exp_maskPhase_sq line 618
  63. lemma OAI.SKQAOA.SiteHistories.prod_union_root line 633
  64. theorem OAI.SKQAOA.SiteHistories.partition_eq_marked line 649
  65. theorem OAI.SKQAOA.SiteHistories.cluster_eq_mixedDifference line 677
  66. theorem OAI.SKQAOA.SiteHistories.cluster_eq_zero line 696
  67. theorem OAI.SKQAOA.SiteHistories.marked_eq_sum_clusters line 704