OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ActiveGibbs.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldActiveGibbs.splitCoordinateWeight line 16
  2. def OAI.MatrixMultiplication.AllFieldActiveGibbs.splitPotential line 20
  3. def OAI.MatrixMultiplication.AllFieldActiveGibbs.splitNormalizer line 24
  4. def OAI.MatrixMultiplication.AllFieldActiveGibbs.splitLogNormalizer line 27
  5. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitCoordinateWeight_pos line 30
  6. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitNormalizer_pos line 36
  7. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitWeight_log line 42
  8. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_log line 51
  9. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_positive_iff line 67
  10. def OAI.MatrixMultiplication.AllFieldActiveGibbs.physicalPotential line 78
  11. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_log_physical line 82
  12. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_positive_has_branch line 98
  13. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_branch_log line 110
  14. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_branch_log line 126
  15. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_log line 142
  16. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_log line 152
  17. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.mem_shapes_of_total line 162
  18. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.mem_below_iff line 174
  19. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.splitShape_exhaustive line 185
  20. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.branchShape_exhaustive line 200
  21. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_positive line 232
  22. theorem OAI.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_positive line 242