OAI/MathematicalPhysics/TensorNetwork/VectorColumn.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialPEPS.Vertex line 13
  2. abbrev OAI.PolynomialPEPS.Edge line 17
  3. abbrev OAI.PolynomialPEPS.IncidentEdge line 22
  4. abbrev OAI.PolynomialPEPS.Configuration line 25
  5. abbrev OAI.PolynomialPEPS.State line 26
  6. abbrev OAI.PolynomialPEPS.Operator line 27
  7. def OAI.PolynomialPEPS.SupportedOn line 31
  8. def OAI.PolynomialPEPS.outer line 40
  9. def OAI.PolynomialPEPS.act line 44
  10. def OAI.PolynomialPEPS.phase line 47
  11. def OAI.PolynomialPEPS.normalized line 49
  12. def OAI.PolynomialPEPS.UniqueGroundVector line 53
  13. def OAI.PolynomialPEPS.GlobalGap line 61
  14. structure OAI.PolynomialPEPS.PEPS line 68
  15. def OAI.PolynomialPEPS.PEPS.contract line 78
  16. def OAI.PolynomialPEPS.PEPS.maxBondDim line 83
  17. def OAI.PolynomialPEPS.PhaseErrorAtMost line 91
  18. theorem OAI.PolynomialPEPS.norm_phase line 98
  19. theorem OAI.PolynomialPEPS.phase_neg_mul line 101
  20. theorem OAI.PolynomialPEPS.phase_arg_mul line 105
  21. theorem OAI.PolynomialPEPS.exists_phase_minimizer line 114
  22. theorem OAI.PolynomialPEPS.norm_normalized line 137
  23. theorem OAI.PolynomialPEPS.act_sub line 142
  24. theorem OAI.PolynomialPEPS.act_smul line 147
  25. theorem OAI.PolynomialPEPS.act_one line 152
  26. theorem OAI.PolynomialPEPS.act_outer line 157
  27. def OAI.PolynomialPEPS.expectation line 168
  28. theorem OAI.PolynomialPEPS.expectation_nonneg line 171
  29. theorem OAI.PolynomialPEPS.globalGap_expectation line 177
  30. theorem OAI.PolynomialPEPS.energy_vector line 194
  31. theorem OAI.PolynomialPEPS.phaseErrorAtMost_iff_exists line 225
  32. def OAI.PolynomialPEPS.productState line 235
  33. def OAI.PolynomialPEPS.productPEPS line 239
  34. theorem OAI.PolynomialPEPS.productPEPS_contract line 244
  35. theorem OAI.PolynomialPEPS.maxBondDim_le_iff line 252
  36. theorem OAI.PolynomialPEPS.productPEPS_bond_bound line 257
  37. theorem OAI.PolynomialPEPS.normalized_dist_le line 266
  38. theorem OAI.PolynomialPEPS.normalized_smul_phase line 291
  39. theorem OAI.PolynomialPEPS.column_of_relative_error line 309
  40. theorem OAI.PolynomialPEPS.column_from_sum_sq_error line 345