OAI/LinearAlgebra/MatrixFields/Extraction/ConditionalLabels.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageRefinementCount line 25
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageNodeCounts line 29
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageRefinementCount_eq_nodeProduct line 33
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageRefinementCount_eq_sourcePoolProduct line 47
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageRefinementCount_pos line 54
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageConditionalWords_card line 59
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageConditionalPool_card line 71
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageConditionalWords_nonempty line 82
9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageEntropyRate line 92
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageEntropyRate_nonneg line 95
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.tendsto_log_stageRefinementCount_div line 100
12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageCost line 107
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.tendsto_log_stageCost_div line 110
14. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stagePairingProduct line 118
15. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryBudget line 122
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stagePairingProduct_succ line 126
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryBudget_succ line 133
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stagePairingProduct_eq_exactWords_card line 140
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stagePairingProduct_le_budget line 150
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryBudget_pos line 157
21. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.StageAuxiliaryCoordinates line 163
22. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryTensor line 174
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryTensor_rankAtMost line 181
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.stageAuxiliaryTensor_borderRankAtMost line 192
25. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.StagePairingCoordinates line 198
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.card_stagePairingCoordinates line 201
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.sum_stageEntropyRate_eq_nodeEntropyTotal line 207
28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.sum_stageEntropyRate_eq_source line 218
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.tendsto_log_stageAuxiliaryBudget_div line 225
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.tendsto_log_stagePairingProduct line 237
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.tendsto_log_stageAuxiliaryBudget line 247
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.StageHierarchyResources.source_stage_resource_rates line 263
33. inductive OAI.MatrixAllFields.MatrixMultiplication.ReaderPair line 304
34. instance OAI.MatrixAllFields.MatrixMultiplication.(instance at line 308) line 308
35. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingSize line 320
36. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingRate line 324
37. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingSize_pos line 328
38. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingRate_nonneg line 337
39. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingSize_product line 346
40. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.pairingRate_sum line 354
41. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_pairingSize line 362
42. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stagePairingSize line 389
43. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stagePairingRate line 393
44. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stagePairingSize_product line 397
45. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stagePairingRate_sum line 407
46. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize line 416
47. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize_normalized line 424
48. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.auxiliary_overhead_tendsto_zero line 434
49. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.auxiliary_overhead_nonneg line 445
50. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.charged_cost_tendsto line 457
51. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.limit_le_source_cost line 467
52. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.lawPairingRate line 479
53. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.lawPairingRate_sum line 484
54. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.incident_rate_eq_prefix_entropy line 494
55. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.remaining_rate_eq_entropy_sub_prefix line 541