OAI/MathematicalPhysics/PEPSSubvolume/Crossing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Singular-safe local crossing and modular substitution identities.

  1. def OAI.PolynomialPEPS.Subvolume.CrossingIdentity.inverseOnSupport line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.inverse_mul_add_kernel line 30
  3. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.commute_prefix line 41
  4. def OAI.PolynomialPEPS.Subvolume.CrossingIdentity.residual line 49
  5. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.inserted_add_residual line 52
  6. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.adjacent_replacement line 70
  7. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.optimizer_residual_zero line 93
  8. theorem OAI.PolynomialPEPS.Subvolume.CrossingIdentity.optimizer_modular_substitution line 140