OAI/MathematicalPhysics/PEPSMove/Optimizer.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_real line 16
  2. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_power_real line 24
  3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_two_powers line 32
  4. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_sub_of_hermitian line 54
  5. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_real_hermitian line 62
  6. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.root_hs_identity line 70
  7. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.root_hs_le_deficit line 105
  8. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.mgf_lower line 130
  9. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_left_real_power line 137
  10. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_root_cycle line 156
  11. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_root_one line 163
  12. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.self_filter_trace line 173
  13. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.petz_diagonal_lower line 182
  14. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.one_filter_self_lower line 212
  15. def OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizerWeights line 255
  16. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizerWeights_nonneg line 259
  17. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizerWeights_sum line 265
  18. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizer_scalar line 271
  19. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizer_factor line 279
  20. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizer_trace_factor line 297
  21. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.gramMoment_pos_of_filter_pos line 309
  22. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizer_attains line 323
  23. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.optimizer_root_bound line 340
  24. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.density_spectrum_sum line 388
  25. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.conditional_optimizer_root_stability line 405