OAI/LinearAlgebra/MatrixFields/Entropy/ConstructionRates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSourceRates.tendsto_log_linear_div_nat line 17
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSourceRates.tendsto_log_polynomial_overhead line 45
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSourceRates.tendsto_log_exponential_source line 63
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSourceRates.log_rankBudget line 75
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSourceRates.tendsto_log_rankBudget line 88
6. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.Copies line 121
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_copies line 125
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_copies_range line 139
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_copies_pos line 149
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.copies_subexponential line 152
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.copies_rate line 163
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.source_rank_rate line 174
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.source_rank_terminal_rate line 192
14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.source_rank_terminal_rate_of_cardinality line 201