OAI/MathematicalPhysics/PEPSSubvolume/PinnedCosts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Feasible pinned filters, positive sector costs and entropy invariance.

  1. theorem OAI.PolynomialPEPS.Subvolume.Pinning.foldl_pin line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.Pinning.commute_foldl line 40
  3. theorem OAI.PolynomialPEPS.Subvolume.Pinning.foldl_pin_nonempty line 48
  4. def OAI.PolynomialPEPS.Subvolume.Pinning.insertedFilter line 59
  5. theorem OAI.PolynomialPEPS.Subvolume.Pinning.insertedFilter_feasible line 65
  6. theorem OAI.PolynomialPEPS.Subvolume.Pinning.inserted_filter_product line 79
  7. theorem OAI.PolynomialPEPS.Subvolume.Pinning.inserted_filteredVector line 98
  8. def OAI.PolynomialPEPS.Subvolume.Pinning.pinnedVector line 108
  9. def OAI.PolynomialPEPS.Subvolume.Pinning.normalizedPinned line 112
  10. theorem OAI.PolynomialPEPS.Subvolume.Pinning.normalizedPinned_norm line 116
  11. theorem OAI.PolynomialPEPS.Subvolume.Pinning.shell_filter_bound line 122
  12. theorem OAI.PolynomialPEPS.Subvolume.Pinning.common_filter_bound_pos line 142
  13. theorem OAI.PolynomialPEPS.Subvolume.Pinning.pinned_sector_cost line 157
  14. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.entropy_unitary_conjugate line 188
  15. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.entropy_concave_mixture line 200