OAI/MathematicalPhysics/PEPSSubvolume/OptimizerEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quadratic crossing bounds for a global filter optimizer.

  1. theorem OAI.PolynomialPEPS.Subvolume.OptimizerEnergy.filter_spectral_sum line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.OptimizerEnergy.spectral_real_error_le line 43
  3. theorem OAI.PolynomialPEPS.Subvolume.OptimizerEnergy.crossing_error_le line 77