OAI/MathematicalPhysics/PEPSFilters/UnitaryVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Unitary first variations and trace stationarity.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.deriv_conjugation_clm line 19
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.stationary_of_unitary_max_clm line 31
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.stationary_of_unitary_max line 76
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.deriv_conjugation_matrix line 107
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.re_inner_deriv_eq_zero_of_max line 117
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.hermitian_of_skew_trace line 149
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.trace_re_hermitian_skew line 171
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.commute_of_unitary_trace_stationarity line 182