OAI/MathematicalPhysics/PEPSMove/Interpolation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare line 15
  2. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_nonneg line 18
  3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_trace line 22
  4. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.entry_le_op line 27
  5. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_norm_le line 37
  6. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_mul_sq_le line 45
  7. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_unitary_left line 61
  8. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.norm_scalar_realpart line 72
  9. def OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.dual line 85
  10. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.dual_left_norm_trace line 89
  11. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_unitary_right line 119
  12. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.dual_hsSquare_right line 129
  13. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.dual_norm_le line 152
  14. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.differentiable_dual line 177
  15. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.interpolation_test line 190
  16. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_conjTranspose line 237
  17. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_mul_le_left line 241
  18. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_mul_le_right line 259
  19. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.scalar_add line 265
  20. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_add line 271
  21. def OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.stripProduct line 279
  22. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.differentiable_stripProduct line 282
  23. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.stripProduct_left line 289
  24. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.stripProduct_right line 296
  25. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.norm_power_strip line 310
  26. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.stripProduct_bounded line 327
  27. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.scalar_star line 336
  28. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_conjTranspose line 342
  29. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.stripProduct_hsSquare_one line 348