OAI/LinearAlgebra/MatrixFields/Entropy/ZeroLeafRates.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder line 18
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_eq line 21
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_zero line 25
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_stirling line 28
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_factorialLogRemainder_div line 39
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_factorialLogRemainder_mul_div line 64
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_succ line 83
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.nat_mul_log_increment_le_one line 92
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.one_le_succ_mul_log_increment line 106
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_nonneg line 119
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_le_one_add_log_pos line 127
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.factorialLogRemainder_le_one_add_log line 137
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.abs_factorialLogRemainder_le line 148
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_multinomial line 166
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_div_scalar line 184
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_nat_normalize line 194
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_multinomial_eq_main_add_remainder line 210
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_multinomial_eq_entropy_add_remainder line 221
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_multinomial_sub_entropy_eq_remainder line 233
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.abs_log_multinomial_sub_entropy_le line 251
21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.abs_log_multinomial_div_sub_entropy_le line 288
22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_one_add_log_succ_div line 313
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_multinomial_div_sub_entropy line 334
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_multinomial_of_empirical_tendsto line 353
25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.mul_log_mul line 366
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_multinomial_mul_eq line 378
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_multinomial_mul line 398
28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_multinomial_repetitions line 437
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_exactWords_card_mul line 448
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.abs_log_exactWords_card_sub_entropy_le line 457
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_card_le_entropy_of_injective_exactWords line 465
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.log_card_div_le_entropy_of_injective_exactWords line 480
33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_log_exactWords_card_of_empirical_tendsto line 494
34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.exists_exactWords_entropy_limit line 508
35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost_pos line 539
36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.population_le_poolAuxiliaryCost line 545
37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost_le_gridGroupOrder line 551
38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.tendsto_log_poolAuxiliaryCost_div_nat line 558
39. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.populationEntropyRate line 580
40. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_multinomial_mul_div_repetition line 584
41. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.populationEntropyRate_nonneg line 614
42. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.poolTypeCount line 628
43. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.poolEntropyTotal line 631
44. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct line 634
45. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.gridProduct line 637
46. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.auxiliaryProduct line 640
47. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.poolTypeCount_pos line 644
48. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_le_auxiliaryProduct line 647
49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.auxiliaryProduct_le_gridProduct line 652
50. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_poolTypeCount_div line 658
51. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_pairingProduct_div line 663
52. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_gridProduct_div line 670
53. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_auxiliaryProduct_div line 678
54. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.pushforwardCounts_mul line 694
55. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.sourcePrefixCounts_mul line 706
56. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.PrefixPool line 712
57. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.sourcePoolCounts line 715
58. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_source_eq line 719
59. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.pairingProduct_source_eq_exactWords_card line 748
60. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.source_poolEntropyTotal_eq line 755
61. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.normalized_of_per_repetition line 766
62. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_pairingProduct line 780
63. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_gridProduct line 790
64. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.tendsto_log_source_auxiliaryProduct line 801
65. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.HierarchySeparationRates.rationalLaw_exists_source_rates line 812
66. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafRates.log_card_supported line 860
67. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafRates.log_card line 878
68. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafRates.tendsto_log_card_supported line 887
69. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafRates.tendsto_log_card line 914
70. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.fourWords line 937
71. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.twoWords line 941
72. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.twoWordsFintype line 945
73. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.multiplicity_pos line 950
74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.four_supported line 953
75. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.two_supported line 967
76. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.four_card_pos line 981
77. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.two_card_pos line 994
78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.four_tendsto_log_card line 1007
79. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.two_tendsto_log_card line 1020