OAI/LinearAlgebra/MatrixMultiplication/Entropy/BaseConditionalReaders.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. def OAI.MatrixMultiplication.BaseConditionalReaders.ConditionalLeaf line 19
  2. def OAI.MatrixMultiplication.BaseConditionalReaders.view line 22
  3. theorem OAI.MatrixMultiplication.BaseConditionalReaders.conditional_flag line 25
  4. def OAI.MatrixMultiplication.BaseConditionalReaders.trivialSchedule line 29
  5. theorem OAI.MatrixMultiplication.BaseConditionalReaders.trivialSchedule_complete line 43
  6. def OAI.MatrixMultiplication.BaseConditionalReaders.binarySchedule line 49
  7. theorem OAI.MatrixMultiplication.BaseConditionalReaders.binarySchedule_complete line 81
  8. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseTwo_subsingleton line 90
  9. def OAI.MatrixMultiplication.BaseConditionalReaders.baseTwo line 114
  10. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseTwo_complete line 118
  11. def OAI.MatrixMultiplication.BaseConditionalReaders.aChoice line 121
  12. def OAI.MatrixMultiplication.BaseConditionalReaders.bChoice line 124
  13. theorem OAI.MatrixMultiplication.BaseConditionalReaders.aChoice_read line 127
  14. theorem OAI.MatrixMultiplication.BaseConditionalReaders.bChoice_read line 133
  15. theorem OAI.MatrixMultiplication.BaseConditionalReaders.aChoice_injective line 139
  16. theorem OAI.MatrixMultiplication.BaseConditionalReaders.bChoice_injective line 154
  17. def OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeA line 169
  18. def OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeB line 176
  19. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeA_complete line 183
  20. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeB_complete line 187
  21. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeC_subsingleton line 191
  22. def OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeC line 202
  23. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeC_complete line 206
  24. def OAI.MatrixMultiplication.BaseConditionalReaders.baseTwoProgram line 209
  25. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseTwoProgram_complete line 219
  26. def OAI.MatrixMultiplication.BaseConditionalReaders.aLabel line 229
  27. def OAI.MatrixMultiplication.BaseConditionalReaders.bLabel line 233
  28. def OAI.MatrixMultiplication.BaseConditionalReaders.aRead line 237
  29. def OAI.MatrixMultiplication.BaseConditionalReaders.bRead line 243
  30. theorem OAI.MatrixMultiplication.BaseConditionalReaders.aRead_correct line 249
  31. theorem OAI.MatrixMultiplication.BaseConditionalReaders.bRead_correct line 263
  32. def OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeProgram line 277
  33. theorem OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeProgram_complete line 295
  34. def OAI.MatrixMultiplication.BaseConditionalReaders.baseTwoReadable line 324
  35. def OAI.MatrixMultiplication.BaseConditionalReaders.baseThreeReadable line 332