OAI/MathematicalPhysics/PEPSSubvolume/UnitaryGauge.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Outward unitary gauges for nested physical filters.

  1. theorem OAI.PolynomialPEPS.Subvolume.SupportedOn.mono line 18
  2. theorem OAI.PolynomialPEPS.Subvolume.exists_local_unitary line 22
  3. theorem OAI.PolynomialPEPS.Subvolume.posSemidef_unitary_conj line 37
  4. theorem OAI.PolynomialPEPS.Subvolume.eigenvalues_unitary_conj line 42
  5. def OAI.PolynomialPEPS.Subvolume.orderedPrefix line 51
  6. theorem OAI.PolynomialPEPS.Subvolume.orderedPrefix_zero line 55
  7. theorem OAI.PolynomialPEPS.Subvolume.orderedPrefix_succ line 56
  8. theorem OAI.PolynomialPEPS.Subvolume.orderedPrefix_unitary line 59
  9. theorem OAI.PolynomialPEPS.Subvolume.orderedPrefix_supported line 65
  10. def OAI.PolynomialPEPS.Subvolume.liftUnitary line 74
  11. def OAI.PolynomialPEPS.Subvolume.outwardPrefix line 86
  12. theorem OAI.PolynomialPEPS.Subvolume.outwardPrefix_spec line 96
  13. def OAI.PolynomialPEPS.Subvolume.gaugedMatrix line 110
  14. theorem OAI.PolynomialPEPS.Subvolume.gaugedMatrix_posSemidef line 115
  15. theorem OAI.PolynomialPEPS.Subvolume.gaugedMatrix_eigenvalues line 119
  16. theorem OAI.PolynomialPEPS.Subvolume.liftLocal_gaugedMatrix line 124
  17. theorem OAI.PolynomialPEPS.Subvolume.gaugeStep_eq line 131
  18. theorem OAI.PolynomialPEPS.Subvolume.orderedPrefix_gauge line 137
  19. theorem OAI.PolynomialPEPS.Subvolume.norm_asMap_unitary line 149
  20. theorem OAI.PolynomialPEPS.Subvolume.norm_asMap_mul_of_unitary line 154
  21. theorem OAI.PolynomialPEPS.Subvolume.norm_orderedPrefix_gauge line 161