OAI/LinearAlgebra/MatrixFields/Extraction/ComplexLabelHierarchySeparation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.populationCoordinateEquiv line 25
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.tensor_transport line 32
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.bankTensor_population_reindex line 41
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.bankTensor_population_rankAtMost line 56
5. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.BankOccurrences line 66
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_bank_product line 69
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_pairing_card line 75
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_bank_rankAtMost line 81
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.occurrence_product line 94
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_population_product line 101
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_population_bank_equiv line 110
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.prefix_separation_identity line 132
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.prefix_separation_rankAtMost line 156
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.separated_coefficient line 173
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.deterministic_separation_identity line 179
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.separated_prefix_synchronized line 188
17. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolEnumeration line 212
18. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode line 216
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode_decode line 223
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode_agree line 232
21. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost line 245
22. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.PoolAuxiliaryGroup line 248
23. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryTensor line 257
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryTensor_rankAtMost line 262
25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_mem_restrictionOrbit line 275
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_raw_prefix_synchronized line 303
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_rankAtMost line 328
28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_borderRankAtMost line 363
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_optimized_pullback line 403
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_optimized_mem_restrictionOrbit line 443
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.shared_branch_rankAtMost line 468
32. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.AuxiliaryCoordinates line 495
33. instance OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryCoordinatesFintype line 499
34. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryTensor line 507
35. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.sourceCoordinate line 513
36. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryCoordinate line 518
37. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor line 523
38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_eq_shared_bank line 533
39. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryTensor_rankAtMost line 557
40. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_rankAtMost line 572
41. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_borderRankAtMost line 585