OAI/MathematicalPhysics/PEPSMove/GridStates.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialPEPS.PhysicalMove.Vertex line 13
  2. def OAI.PolynomialPEPS.PhysicalMove.ForwardAdjacent line 15
  3. abbrev OAI.PolynomialPEPS.PhysicalMove.Edge line 19
  4. instance OAI.PolynomialPEPS.PhysicalMove.edgeFintype line 21
  5. def OAI.PolynomialPEPS.PhysicalMove.Incident line 23
  6. abbrev OAI.PolynomialPEPS.PhysicalMove.IncidentEdge line 26
  7. instance OAI.PolynomialPEPS.PhysicalMove.incidentFintype line 27
  8. abbrev OAI.PolynomialPEPS.PhysicalMove.Configuration line 30
  9. abbrev OAI.PolynomialPEPS.PhysicalMove.State line 31
  10. abbrev OAI.PolynomialPEPS.PhysicalMove.Operator line 32
  11. abbrev OAI.PolynomialPEPS.PhysicalMove.RegionConfiguration line 33
  12. def OAI.PolynomialPEPS.PhysicalMove.liftLocal line 37
  13. def OAI.PolynomialPEPS.PhysicalMove.SupportedOn line 44
  14. def OAI.PolynomialPEPS.PhysicalMove.EdgeSites line 48
  15. def OAI.PolynomialPEPS.PhysicalMove.Hamiltonian line 50
  16. def OAI.PolynomialPEPS.PhysicalMove.asMap line 54
  17. def OAI.PolynomialPEPS.PhysicalMove.opNorm line 57
  18. def OAI.PolynomialPEPS.PhysicalMove.IsGridHamiltonian line 60
  19. def OAI.PolynomialPEPS.PhysicalMove.phase line 66
  20. def OAI.PolynomialPEPS.PhysicalMove.UniqueGround line 69
  21. def OAI.PolynomialPEPS.PhysicalMove.FullSystemGap line 79
  22. abbrev OAI.PolynomialPEPS.PhysicalMove.LocalTensor line 86
  23. def OAI.PolynomialPEPS.PhysicalMove.contractPEPS line 91
  24. def OAI.PolynomialPEPS.PhysicalMove.HasPEPSApproximation line 96
  25. def OAI.PolynomialPEPS.PhysicalMove.MainStatement line 107
  26. def OAI.PolynomialPEPS.PhysicalMove.joinConfigurations line 129
  27. def OAI.PolynomialPEPS.PhysicalMove.coefficientMatrix line 137
  28. def OAI.PolynomialPEPS.PhysicalMove.reducedDensity line 143
  29. theorem OAI.PolynomialPEPS.PhysicalMove.reducedDensity_isHermitian line 147
  30. def OAI.PolynomialPEPS.PhysicalMove.vonNeumannEntropy line 153
  31. def OAI.PolynomialPEPS.PhysicalMove.boundaryCard line 158
  32. def OAI.PolynomialPEPS.PhysicalMove.UniformAreaLaw line 166