OAI/MathematicalPhysics/PEPSSubvolume/OptimizerExistence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Attained positive Schatten-filter maxima by compactness.

  1. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.compact_unitary line 28
  2. abbrev OAI.PolynomialPEPS.Subvolume.OptimizerExistence.Parameters line 36
  3. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.parameters_compact line 40
  4. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.parameters_nonempty line 47
  5. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.spectral_positive line 51
  6. def OAI.PolynomialPEPS.Subvolume.OptimizerExistence.fromParameters line 57
  7. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.fromParameters_feasible line 62
  8. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.fromParameters_continuous line 73
  9. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.represent_filter line 86
  10. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.filter_ext line 110
  11. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.continuous_liftLocal line 117
  12. lemma OAI.PolynomialPEPS.Subvolume.OptimizerExistence.continuous_filtered_parameters line 129
  13. theorem OAI.PolynomialPEPS.Subvolume.OptimizerExistence.exists_optimizer line 151