OAI/LinearAlgebra/MatrixFields/Extraction/JointTypeCounts.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.invariant_incidence_count line 24
2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.invariant_incidence_degree_eq line 56
3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.invariant_incidence_degree_le_exp line 70
4. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.FixedClassWords line 103
5. def OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedWordsEquiv line 106
6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedClassWords_card line 130
7. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.ClassExactWords line 141
8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.classExactWords_card line 143
9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.classExactWords_card_pos line 149
10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.classExactWords_card_mul_factorials line 154
11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedClassWords_transitive line 165
12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.log_classExactWords_card line 176
13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.log_classExactWords_card_eq_factorials line 183
14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.abs_log_classExactWords_card_sub_entropy_le line 189
15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.abs_log_fixedClassWords_card_sub_entropy_le line 199
16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.tendsto_log_classExactWords_card_div line 209
17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.pushforwardCounts_eq_sum line 240
18. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.FixedCoarseWords line 248
19. def OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedCoarseWordsEquiv line 251
20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedCoarseWords_card line 298
21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.fixedCoarseWords_card_pos line 308
22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.exactWords_card_eq_coarse_mul_fixed line 314
23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.log_fixedCoarseWords_card line 333
24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.log_fixedCoarseWords_card_eq_factorials line 348
25. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.abs_log_fixedCoarseWords_card_sub_entropy_le line 358
26. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.card_allowed_over_coarse_le line 382
27. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.card_entropy_bounded_words_le line 468
28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.card_class_entropy_bounded_words_le line 545
29. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.marginal_coordinate_error line 560
30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.designated_coordinate_error line 569
31. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.residual_window_error line 589
32. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.exists_entropy_window line 608
33. theorem OAI.MatrixAllFields.MatrixMultiplication.JointTypeCounts.exists_window_word_count line 621