OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexHierarchySeparationRates.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost_pos line 19
  2. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.population_le_poolAuxiliaryCost line 25
  3. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost_le_gridGroupOrder line 31
  4. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.tendsto_log_poolAuxiliaryCost_div_nat line 38
  5. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.populationEntropyRate line 60
  6. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_multinomial_mul_div_repetition line 64
  7. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.populationEntropyRate_nonneg line 94
  8. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.poolTypeCount line 108
  9. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.poolEntropyTotal line 111
  10. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct line 114
  11. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.gridProduct line 117
  12. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.auxiliaryProduct line 120
  13. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.poolTypeCount_pos line 124
  14. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_le_auxiliaryProduct line 127
  15. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.auxiliaryProduct_le_gridProduct line 132
  16. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_poolTypeCount_div line 138
  17. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_pairingProduct_div line 143
  18. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_gridProduct_div line 150
  19. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_auxiliaryProduct_div line 158
  20. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.pushforwardCounts_mul line 174
  21. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.sourcePrefixCounts_mul line 186
  22. abbrev OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.PrefixPool line 192
  23. def OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.sourcePoolCounts line 195
  24. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_source_eq line 199
  25. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_source_eq_exactWords_card line 228
  26. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.source_poolEntropyTotal_eq line 235
  27. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.normalized_of_per_repetition line 246
  28. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_pairingProduct line 260
  29. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_gridProduct line 270
  30. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_auxiliaryProduct line 281
  31. theorem OAI.MatrixMultiplication.Foundation.HierarchySeparationRates.rationalLaw_exists_source_rates line 292