OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexConditionalPrefixWords.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. instance OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.labelRecordZero_subsingleton line 18
  2. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.population_fst line 23
  3. abbrev OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.ExactPrefix line 43
  4. abbrev OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalPool line 50
  5. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalFinset line 54
  6. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.mem_conditionalFinset line 60
  7. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalFinsetEquiv line 67
  8. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalPool_card line 71
  9. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalFinset_card line 75
  10. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalFinsetEquivFin line 79
  11. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.conditionalPoolEquivFin line 85
  12. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.decodedFine_eq_geometryDecode line 89
  13. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendPrefix line 97
  14. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendPrefix_val line 108
  15. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.oldPrefix line 112
  16. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.oldPrefix_val line 134
  17. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.finePrefix line 137
  18. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.finePrefix_val line 153
  19. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.oldPrefix_appendPrefix line 156
  20. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.nextPrefixSigmaEquiv line 161
  21. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.nextPrefixEquiv line 175
  22. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendCode line 182
  23. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendCode_val line 187
  24. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.nextPrefixEquiv_symm_apply line 192
  25. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.nextPrefixEquiv_appendCode line 197
  26. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendCode_injective line 203
  27. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.appendCode_surjective line 208
  28. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.decodedFine_mem_conditionalFinset line 213
  29. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.rootPopulation line 222
  30. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.rootPrefixWord line 231
  31. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.rootPrefixWord_val line 247
  32. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.rootPrefixEquiv line 251
  33. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.prefixSymbol_in_source_range line 271
  34. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourceSymbol line 282
  35. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourceSymbol_record line 285
  36. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourceSymbol_eq_iff line 289
  37. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourceSymbol_grade line 299
  38. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.decodeSourceWord line 306
  39. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.encodeSourceWord line 321
  40. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.encodeSourceWord_val line 340
  41. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourceSymbol_encodeSourceWord line 346
  42. def OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourcePrefixEquiv line 352
  43. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourcePrefixEquiv_apply_val line 367
  44. theorem OAI.MatrixMultiplication.Foundation.ConditionalPrefixWords.sourcePrefixEquiv_symm_val line 373