OAI/LinearAlgebra/MatrixMultiplication/Duality/LawEntropy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. def OAI.MatrixMultiplication.DualLawEntropy.allCenter line 23
  2. theorem OAI.MatrixMultiplication.DualLawEntropy.iid_allowed line 26
  3. theorem OAI.MatrixMultiplication.DualLawEntropy.not_event_iff_allCenter line 39
  4. theorem OAI.MatrixMultiplication.DualLawEntropy.event_sum_congr line 57
  5. theorem OAI.MatrixMultiplication.DualLawEntropy.removed_event_mass_eq line 67
  6. theorem OAI.MatrixMultiplication.DualLawEntropy.removed_event_entropy_eq line 79
  7. def OAI.MatrixMultiplication.DualLawEntropy.centerWordEquiv line 97
  8. theorem OAI.MatrixMultiplication.DualLawEntropy.center_word_mass line 104
  9. theorem OAI.MatrixMultiplication.DualLawEntropy.allCenter_mass line 120
  10. theorem OAI.MatrixMultiplication.DualLawEntropy.allCenter_entropy line 130
  11. theorem OAI.MatrixMultiplication.DualLawEntropy.conditionalCompletionLaw_entropy line 145