OAI/MathematicalPhysics/PEPSMove/Purification.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy_neg line 17
  2. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.unitary_distance_four line 21
  3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.renyi_deficit_nonneg line 34
  4. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.opposite_entropy_absorbed line 56
  5. def OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.uncoefficient line 124
  6. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.coefficient_uncoefficient line 128
  7. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.uncoefficient_gram line 132
  8. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.ptrL_density line 138
  9. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.traceEntropy_diagonal line 142
  10. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.conditionalEntropy_eq line 174
  11. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.gram_root line 182
  12. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.one_filter_purification_bound line 198