OAI/MathematicalPhysics/PEPSSubvolume/Marginal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact optimizing marginal identities including singular filters.

  1. theorem OAI.PolynomialPEPS.Subvolume.OptimizerMarginal.optimizer_trace_moment line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.OptimizerMarginal.optimizer_marginal_commute line 45
  3. theorem OAI.PolynomialPEPS.Subvolume.OptimizerMarginal.optimizer_marginal_spectral line 74