OAI/MathematicalPhysics/PEPSSubvolume/LocalOperators.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Local extensions, tensor coordinates and exact support adapters.

  1. theorem OAI.PolynomialPEPS.Subvolume.joinConfigurations_left line 15
  2. theorem OAI.PolynomialPEPS.Subvolume.joinConfigurations_right line 20
  3. def OAI.PolynomialPEPS.Subvolume.joinEquiv line 25
  4. theorem OAI.PolynomialPEPS.Subvolume.joinEquiv_apply line 35
  5. theorem OAI.PolynomialPEPS.Subvolume.joinEquiv_symm_join line 39
  6. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_join line 44
  7. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_eq_reindex line 69
  8. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_zero line 82
  9. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_add line 89
  10. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_smul line 97
  11. def OAI.PolynomialPEPS.Subvolume.localLiftHom line 105
  12. theorem OAI.PolynomialPEPS.Subvolume.opNorm_liftLocal_le line 120
  13. theorem OAI.PolynomialPEPS.Subvolume.asMap_liftLocal_join line 127
  14. theorem OAI.PolynomialPEPS.Subvolume.reducedDensity_posSemidef line 138
  15. theorem OAI.PolynomialPEPS.Subvolume.inner_liftLocal_trace line 142
  16. def OAI.PolynomialPEPS.Subvolume.restrictRegion line 162
  17. def OAI.PolynomialPEPS.Subvolume.liftBetween line 166
  18. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_liftBetween line 173
  19. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_injective line 192
  20. def OAI.PolynomialPEPS.Subvolume.liftBetweenHom line 197