OAI/MathematicalPhysics/PEPSFilters/Basic.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Square-grid states, Hamiltonians, PEPS and nested positive filters.

  1. abbrev OAI.PolynomialPEPS.PinnedEntropy.Vertex line 12
  2. def OAI.PolynomialPEPS.PinnedEntropy.ForwardAdjacent line 14
  3. abbrev OAI.PolynomialPEPS.PinnedEntropy.Edge line 18
  4. instance OAI.PolynomialPEPS.PinnedEntropy.edgeFintype line 20
  5. def OAI.PolynomialPEPS.PinnedEntropy.Incident line 22
  6. abbrev OAI.PolynomialPEPS.PinnedEntropy.IncidentEdge line 25
  7. instance OAI.PolynomialPEPS.PinnedEntropy.incidentFintype line 26
  8. abbrev OAI.PolynomialPEPS.PinnedEntropy.Configuration line 29
  9. abbrev OAI.PolynomialPEPS.PinnedEntropy.State line 30
  10. abbrev OAI.PolynomialPEPS.PinnedEntropy.Operator line 31
  11. abbrev OAI.PolynomialPEPS.PinnedEntropy.RegionConfiguration line 32
  12. def OAI.PolynomialPEPS.PinnedEntropy.liftLocal line 35
  13. def OAI.PolynomialPEPS.PinnedEntropy.SupportedOn line 42
  14. def OAI.PolynomialPEPS.PinnedEntropy.EdgeSites line 46
  15. def OAI.PolynomialPEPS.PinnedEntropy.Hamiltonian line 48
  16. def OAI.PolynomialPEPS.PinnedEntropy.asMap line 52
  17. def OAI.PolynomialPEPS.PinnedEntropy.opNorm line 55
  18. def OAI.PolynomialPEPS.PinnedEntropy.IsGridHamiltonian line 57
  19. def OAI.PolynomialPEPS.PinnedEntropy.phase line 63
  20. def OAI.PolynomialPEPS.PinnedEntropy.UniqueGround line 65
  21. def OAI.PolynomialPEPS.PinnedEntropy.FullSystemGap line 74
  22. abbrev OAI.PolynomialPEPS.PinnedEntropy.LocalTensor line 80
  23. def OAI.PolynomialPEPS.PinnedEntropy.contractPEPS line 83
  24. def OAI.PolynomialPEPS.PinnedEntropy.HasPEPSApproximation line 88
  25. def OAI.PolynomialPEPS.PinnedEntropy.MainStatement line 97
  26. def OAI.PolynomialPEPS.PinnedEntropy.joinConfigurations line 109
  27. def OAI.PolynomialPEPS.PinnedEntropy.coefficientMatrix line 115
  28. def OAI.PolynomialPEPS.PinnedEntropy.reducedDensity line 119
  29. theorem OAI.PolynomialPEPS.PinnedEntropy.reducedDensity_isHermitian line 123
  30. def OAI.PolynomialPEPS.PinnedEntropy.vonNeumannEntropy line 127
  31. def OAI.PolynomialPEPS.PinnedEntropy.boundaryCard line 130
  32. def OAI.PolynomialPEPS.PinnedEntropy.UniformAreaLaw line 135
  33. structure OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.PositiveFilter line 151
  34. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.tracePower line 155
  35. abbrev OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.FilterFamily line 159
  36. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Admissible line 162
  37. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.output line 166
  38. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsMaximizer line 171
  39. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.normalizedOutput line 176
  40. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.logCost line 180
  41. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.LowerComparison line 184
  42. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.UpperComparison line 189