OAI/LinearAlgebra/MatrixFields/Parameters/StageCCapacity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal line 17
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal_eq_shapeLaw line 20
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal line 27
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal_symbolic line 31
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_2_1_1_0 line 38
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_2_1_1_1 line 49
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_2_1_1_2 line 60
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_2_1_0 line 71
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_2_1_1 line 82
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_2_1_2 line 93
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_1_2_0 line 104
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_1_2_1 line 115
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq_1_1_2_2 line 126
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.symbolicMarginal_eq line 137
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal_eq line 154
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.entropy_three_points line 165
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.entropy_distinguished line 184
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.entropy_other line 193
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal_entropy line 201
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.stageCMarginal_priority_entropy line 214
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCCapacity.allocation_capacity line 224