OAI/MathematicalPhysics/PEPSFilters/LocalOperators.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Local matrix embeddings, reduced density operators and tensor corners.

  1. def OAI.PolynomialPEPS.PinnedEntropy.restrictConfiguration line 13
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.restrict_join_left line 16
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.restrict_join_right line 22
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.join_restrict line 28
  5. def OAI.PolynomialPEPS.PinnedEntropy.splitConfigurations line 35
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.agree_complement_iff line 42
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_eq_kronecker line 54
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_one line 64
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_mul line 70
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_star line 76
  11. def OAI.PolynomialPEPS.PinnedEntropy.liftLocalHom line 82
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_positive line 101
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_unitary line 107
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_join line 114
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_injective line 125
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_extend line 133
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.SupportedOn.mono line 164
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.SupportedOn.one line 170
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.SupportedOn.mul line 173
  20. lemma OAI.PolynomialPEPS.PinnedEntropy.SupportedOn.star line 179
  21. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_unitary_iff line 184
  22. lemma OAI.PolynomialPEPS.PinnedEntropy.SupportedOn.unitary_rep line 194
  23. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_norm line 207
  24. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_apply line 216
  25. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_apply_join line 220
  26. lemma OAI.PolynomialPEPS.PinnedEntropy.coefficientMatrix_asMap_liftLocal line 229
  27. lemma OAI.PolynomialPEPS.PinnedEntropy.coefficientMatrix_injective line 241
  28. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_eq_trace_coefficient line 248
  29. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_asMap_liftLocal line 257
  30. lemma OAI.PolynomialPEPS.PinnedEntropy.trace_reducedDensity line 265
  31. lemma OAI.PolynomialPEPS.PinnedEntropy.reducedDensity_posSemidef line 270
  32. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_liftLocal_fix_of_mul_density line 274
  33. def OAI.PolynomialPEPS.PinnedEntropy.splitRegion line 290
  34. lemma OAI.PolynomialPEPS.PinnedEntropy.splitRegion_restrict line 302
  35. def OAI.PolynomialPEPS.PinnedEntropy.regionTensor line 307
  36. lemma OAI.PolynomialPEPS.PinnedEntropy.regionTensor_mul line 313
  37. lemma OAI.PolynomialPEPS.PinnedEntropy.regionTensor_star line 319
  38. lemma OAI.PolynomialPEPS.PinnedEntropy.regionTensor_positive line 326
  39. lemma OAI.PolynomialPEPS.PinnedEntropy.regionTensor_trace line 332
  40. lemma OAI.PolynomialPEPS.PinnedEntropy.outside_core_iff line 340
  41. lemma OAI.PolynomialPEPS.PinnedEntropy.outside_shell_iff line 353
  42. lemma OAI.PolynomialPEPS.PinnedEntropy.lift_regionTensor_one_right line 368
  43. lemma OAI.PolynomialPEPS.PinnedEntropy.lift_regionTensor_one_left line 381
  44. lemma OAI.PolynomialPEPS.PinnedEntropy.lift_regionTensor line 394
  45. lemma OAI.PolynomialPEPS.PinnedEntropy.lift_core_shell_commute line 401
  46. def OAI.PolynomialPEPS.PinnedEntropy.regionCornerHom line 409