OAI/LinearAlgebra/MatrixMultiplication/Duality/HiddenRates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. structure OAI.MatrixMultiplication.DualHiddenRates.HiddenInvariant line 23
  2. theorem OAI.MatrixMultiplication.DualHiddenRates.incident_minus_entropy line 31
  3. theorem OAI.MatrixMultiplication.DualHiddenRates.incident_plus_entropy line 53
  4. theorem OAI.MatrixMultiplication.DualHiddenRates.gibbs_entropy line 83
  5. theorem OAI.MatrixMultiplication.DualHiddenRates.minus_hidden line 101
  6. theorem OAI.MatrixMultiplication.DualHiddenRates.plusA_hidden line 116
  7. theorem OAI.MatrixMultiplication.DualHiddenRates.plusC_hidden line 131