OAI/MathematicalPhysics/PEPSSubvolume/Filters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Positive filter families and one-factor global optimization.

  1. abbrev OAI.PolynomialPEPS.Subvolume.LocalPositiveFilter line 15
  2. abbrev OAI.PolynomialPEPS.Subvolume.filterTracePower line 18
  3. abbrev OAI.PolynomialPEPS.Subvolume.FilterFamily line 22
  4. abbrev OAI.PolynomialPEPS.Subvolume.FilterFeasible line 25
  5. def OAI.PolynomialPEPS.Subvolume.orderedFilterProduct line 29
  6. def OAI.PolynomialPEPS.Subvolume.filteredVector line 34
  7. def OAI.PolynomialPEPS.Subvolume.IsFilterOptimizer line 38
  8. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.orderedPrefix_eq_finRange line 50
  9. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.orderedFilterProduct_eq_prefix line 61
  10. theorem OAI.PolynomialPEPS.Subvolume.OptimizerGauge.unitary_positive_family_bound line 75
  11. theorem OAI.PolynomialPEPS.Subvolume.OptimizerGauge.prefix_update_outside line 105
  12. theorem OAI.PolynomialPEPS.Subvolume.OptimizerGauge.prefix_update_add line 113
  13. theorem OAI.PolynomialPEPS.Subvolume.OptimizerGauge.prefix_update_smul line 128
  14. theorem OAI.PolynomialPEPS.Subvolume.OptimizerGauge.one_replacement_bound line 149