OAI/LinearAlgebra/MatrixMultiplication/Duality/Information.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. def OAI.MatrixMultiplication.DualInformation.ConditionalIndependent line 20
  2. def OAI.MatrixMultiplication.DualInformation.ConditionalMassFactorization line 27
  3. theorem OAI.MatrixMultiplication.DualInformation.conditionalIndependent_of_mass_factorization line 35
  4. theorem OAI.MatrixMultiplication.DualInformation.mass_factorization_of_conditionalIndependent line 58
  5. theorem OAI.MatrixMultiplication.DualInformation.conditionalIndependent_iff_mass_factorization line 74
  6. theorem OAI.MatrixMultiplication.DualInformation.joint_append_readable_entropy line 81
  7. def OAI.MatrixMultiplication.DualInformation.remainingEntropy line 106
  8. theorem OAI.MatrixMultiplication.DualInformation.remainingEntropy_zero line 111
  9. theorem OAI.MatrixMultiplication.DualInformation.remainingEntropy_complete line 126
  10. theorem OAI.MatrixMultiplication.DualInformation.prefix_entropy_succ line 135
  11. theorem OAI.MatrixMultiplication.DualInformation.remainingEntropy_succ_readable line 146
  12. theorem OAI.MatrixMultiplication.DualInformation.remainingEntropy_succ_independent line 161
  13. theorem OAI.MatrixMultiplication.DualInformation.incident_rate_eq_coordinate_entropy line 167
  14. theorem OAI.MatrixMultiplication.DualInformation.nonincident_rate_eq_entropy_sub_coordinate line 221