OAI/MathematicalPhysics/PEPSSubvolume/TraceFunctionals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Hermitian trace representatives and spanning by reflections.

  1. theorem OAI.PolynomialPEPS.Subvolume.HermitianFunctional.map_star_of_real line 21
  2. def OAI.PolynomialPEPS.Subvolume.HermitianFunctional.representative line 41
  3. theorem OAI.PolynomialPEPS.Subvolume.HermitianFunctional.apply_eq_trace line 44
  4. theorem OAI.PolynomialPEPS.Subvolume.HermitianFunctional.isHermitian_of_trace_real line 56
  5. theorem OAI.PolynomialPEPS.Subvolume.HermitianFunctional.commuting_transition line 67
  6. theorem OAI.PolynomialPEPS.Subvolume.HermitianFunctional.moment_commute line 84
  7. def OAI.PolynomialPEPS.Subvolume.ReflectionSpan.reflection line 114
  8. theorem OAI.PolynomialPEPS.Subvolume.ReflectionSpan.reflection_star line 127
  9. theorem OAI.PolynomialPEPS.Subvolume.ReflectionSpan.reflection_eq line 135
  10. theorem OAI.PolynomialPEPS.Subvolume.ReflectionSpan.zero_of_hermitian_tests line 145
  11. theorem OAI.PolynomialPEPS.Subvolume.ReflectionSpan.zero_of_reflection_tests line 165