OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexHierarchyEntropy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.map_mass_mul_conditional_map line 17
  2. def OAI.MatrixMultiplication.Foundation.LabelRecord line 37
  3. instance OAI.MatrixMultiplication.Foundation.labelRecordFintype line 41
  4. def OAI.MatrixMultiplication.Foundation.labelRecordOf line 51
  5. structure OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy line 56
  6. def OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw line 64
  7. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_zero_mass line 80
  8. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_succ line 84
  9. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_succ_mass line 90
  10. def OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy line 96
  11. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_eq line 102
  12. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_eq_zero_of_le line 109
  13. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.zero_prefix_contribution line 114
  14. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_entropy_succ line 121
  15. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_entropy line 130
  16. def OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.recordLaw line 141
  17. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.recordLaw_entropy line 144
  18. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_sum_of_injective_record line 149
  19. def OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels line 161
  20. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_prefixLaw_mass line 165
  21. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_refinementEntropy_eq line 191
  22. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_refinementEntropy_sum line 201
  23. theorem OAI.MatrixMultiplication.Foundation.FiniteLabelHierarchy.entropy_eq_sum_conditional_labels line 210