OAI/MathematicalPhysics/PEPSFilters/Bipartite.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Bipartite physical states and finite Schmidt decompositions.

  1. def OAI.PolynomialPEPS.PinnedEntropy.tensorState line 24
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.coefficientMatrix_tensorState line 29
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_tensorState line 35
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_liftLocal_tensorState line 53
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.liftComplement_apply_join line 66
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.coefficientMatrix_asMap_liftComplement line 85
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_liftComplement_tensorState line 97
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_tensorState_productOperator line 112
  9. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.columnVector line 127
  10. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.rowVector line 129
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.inner_columnVector line 133
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.inner_rowVector line 139
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.orthonormal_columns line 144
  14. abbrev OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.schmidtIndex line 151
  15. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.schmidtRight line 155
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.orthonormal_schmidtRight line 159
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.rowVector_zero_of_diagonal_zero line 179
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.schmidt_reconstruct_entry line 186
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.rotated_density_diagonal line 215
  20. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.physical_schmidt_decomposition line 235
  21. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.sum_schmidt_probabilities line 265
  22. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.diagonal_conjugate_column line 287