OAI/MathematicalPhysics/PEPSFilters/FilterStationarity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Local stationarity, trace stripping and commutation of maximizing filters.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.matrixOutput_add line 21
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.matrixOutput_smul line 29
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.matrixOutput_update_add line 37
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.matrixOutput_update_smul line 62
  5. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.insertionMap line 87
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.insertionMap_self line 96
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsMaximizer.insertion_unitary_max line 104
  8. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsMaximizer.local_unitary_stationarity line 135
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.trace_strip_local line 170
  10. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.propagateConjugation line 184
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.matrixOutput_propagate line 190
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.propagate_trace_strip line 207
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.output_succ line 230
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.insertionMap_succ_zero line 236
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.insertionMap_succ_succ line 245
  16. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.commute_of_insertion_stationarity line 260
  17. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.IsMaximizer.local_commute_of_invertible line 307