OAI/LinearAlgebra/MatrixFields/Entropy/RectangularGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangular_power_cost_padding_bound line 17
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_power_costs line 45
3. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost line 56
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_zero line 60
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_succ line 63
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_bound line 67
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangular_power_programs_of_block_step line 99
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_block_step line 120