OAI/MathematicalPhysics/PEPSFilters/Regularized.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Regularized spectral coordinates, commuting optimizers and compact limits.

  1. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix line 21
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_zero line 26
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_positive line 31
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_invertible line 39
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_continuous line 51
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_conjugate line 70
  7. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedFilters line 79
  8. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsRegularizedMaximizer line 83
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularized_output_continuous line 89
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.exists_regularized_maximizer line 104
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.insertion_stationarity_of_unitary_max line 119
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsRegularizedMaximizer.insertion_unitary_max line 152
  13. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.exists_regularized_maximizer_commute line 178
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedCoordinateMatrix_jointContinuous line 196
  15. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedRawOutput line 218
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedRawOutput_eq line 222
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedRawOutput_zero line 227
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularizedRawOutput_jointContinuous line 234
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.continuous_reducedDensity line 252
  20. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.isMaximizer_of_coordinate_max line 267
  21. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.exists_maximizer_commute line 290