OAI/MathematicalPhysics/PEPSMove/DoubleCurve.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialPEPS.PhysicalMove.LocalMove.matrixMulCLM line 19
  2. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.matrixMul_differentiable line 33
  3. def OAI.PolynomialPEPS.PhysicalMove.LocalMove.reshuffleCLM line 43
  4. def OAI.PolynomialPEPS.PhysicalMove.LocalMove.flattenCLM line 49
  5. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.flatten_norm_sq line 56
  6. def OAI.PolynomialPEPS.PhysicalMove.LocalMove.doubleCurve line 63
  7. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.doubleCurve_differentiable line 70
  8. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.doubleCurve_bounded line 90
  9. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.doubleCurve_left line 123
  10. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.doubleCurve_right line 149
  11. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.one_copy_interpolation_fullrank line 178