OAI/MathematicalPhysics/PEPSFilters/EnergyOptimizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Regularized and exact maximizing filters with controlled excitation energy.

  1. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.exists_regularized_maximizer_energy line 28
  2. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.exists_maximizer_energy line 62