OAI/MathematicalPhysics/PEPSSubvolume/UnitaryVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Left and right unitary first variations.

  1. theorem OAI.PolynomialPEPS.Subvolume.UnitaryStationarity.real_inner_le_of_norm_le line 24
  2. theorem OAI.PolynomialPEPS.Subvolume.UnitaryStationarity.left_moment_real line 34
  3. theorem OAI.PolynomialPEPS.Subvolume.UnitaryStationarity.right_moment_real line 65