OAI/MathematicalPhysics/PEPSSubvolume/Diagonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Spectral diagonal gradients of actual maximizing filters.

  1. def OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltCost line 25
  2. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltCost_zero line 29
  3. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltCost_pos line 33
  4. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltCost_power line 48
  5. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltCost_derivative line 58
  6. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.tiltScale_derivative line 76
  7. theorem OAI.PolynomialPEPS.Subvolume.DiagonalStationarity.diagonal_moment line 86
  8. theorem OAI.PolynomialPEPS.Subvolume.ActualDiagonal.spectral_positive line 155
  9. theorem OAI.PolynomialPEPS.Subvolume.ActualDiagonal.optimizer_diagonal_moment line 161