OAI/MathematicalPhysics/PEPSMove/LocalOperators.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialPEPS.PhysicalMove.joinConfigurations_left line 13
  2. theorem OAI.PolynomialPEPS.PhysicalMove.joinConfigurations_right line 18
  3. def OAI.PolynomialPEPS.PhysicalMove.joinEquiv line 23
  4. theorem OAI.PolynomialPEPS.PhysicalMove.joinEquiv_apply line 33
  5. theorem OAI.PolynomialPEPS.PhysicalMove.joinEquiv_symm_join line 37
  6. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_join line 42
  7. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_eq_reindex line 68
  8. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_one line 81
  9. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_mul line 88
  10. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_star line 101
  11. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_zero line 110
  12. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_add line 117
  13. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_smul line 125
  14. def OAI.PolynomialPEPS.PhysicalMove.localLiftHom line 134
  15. theorem OAI.PolynomialPEPS.PhysicalMove.opNorm_liftLocal_le line 149
  16. theorem OAI.PolynomialPEPS.PhysicalMove.asMap_liftLocal_join line 156
  17. theorem OAI.PolynomialPEPS.PhysicalMove.reducedDensity_posSemidef line 167
  18. theorem OAI.PolynomialPEPS.PhysicalMove.inner_liftLocal_trace line 172
  19. def OAI.PolynomialPEPS.PhysicalMove.restrictRegion line 193
  20. def OAI.PolynomialPEPS.PhysicalMove.liftBetween line 198
  21. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_liftBetween line 205
  22. theorem OAI.PolynomialPEPS.PhysicalMove.liftLocal_injective line 224
  23. def OAI.PolynomialPEPS.PhysicalMove.liftBetweenHom line 236