OAI/LinearAlgebra/MatrixFields/Entropy/NativeLaws.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.indexedRationalLaw line 18
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageASplitLaw line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBSplitLaw line 33
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.indexedMarginalLaw line 38
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.indexedMarginalLaw_mass line 44
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageAMarginalLaw line 53
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBMarginalLaw line 60
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity_first_entropy line 67
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity_first_entropy line 78
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.halfFiniteLaw line 89
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.littleFiniteLaw line 94
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.list_rat_cast_inline_MatrixMultiplication_AllFieldNativeLaws line 99
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.pairLaw_total line 105
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.pairFiniteLaw line 123
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageAPairLaw line 138
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBPairLaw line 149
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity_sharing line 159
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity_sharing line 168