OAI/LinearAlgebra/MatrixFields/Extraction/JointPairClassWindows.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.wordPopulation line 18
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.wordPopulation_sum line 21
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.wordPopulation_reindex line 26
4. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.ExactWords line 30
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.wordPopulation_sigma_fst line 33
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_nonempty line 45
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.samePopulation_iff_permutation line 54
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.samePopulation_card_mul line 68
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_card line 96
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_card_pos line 110
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_card_le line 114
12. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.PopulationWords line 136
13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.populationWordsEquiv line 139
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.populationWords_card line 158
15. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.ConditionalWords line 163
16. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.fiberWordEquiv line 166
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.wordPopulation_fiber line 178
18. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.conditionalWordsEquiv line 184
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.conditionalWords_card line 196
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.conditionalWords_card_pos line 203
21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.conditionalWords_nonempty line 209
22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.conditionalWords_nonempty_iff line 214
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.multinomial_prod_counts line 230
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_card_prod_counts line 260
25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exactWords_card_eq_coarse_mul_conditional line 266
26. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.pushforwardCounts line 288
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.pushforwardCounts_sum line 293
28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.pushforwardCounts_apply line 301
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.pushforwardCounts_sum_pair line 307
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.pushforwardCounts_factorial_prod_of_injective line 321
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.multinomial_pushforwardCounts_of_injective line 338
32. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.refinementCount line 350
33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.multinomial_succ line 354
34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.pool_multinomial_eq_one_of_zero line 365
35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.multinomial_eq_refinementCount_product line 379
36. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.sourcePrefixCounts line 396
37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.sourcePrefixCounts_compatible line 400
38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.source_refinementCount_product line 407
39. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchyCounts.source_refinementCount_product_eq_exactWords_card line 421
40. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.Fiber line 446
41. def OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.fiberWord line 448
42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.fiber_population line 452
43. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.fiber_card line 475
44. def OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.conditionalCenter line 478
45. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.fiber_window line 482
46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairClassWindows.fiber_count_window line 503