OAI/LinearAlgebra/MatrixFields/Entropy/ComplexPolynomialPowerGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_affine_mul_geometric_zero line 16
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.eventually_affine_mul_pow_le_pow line 23
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.eventually_affine_mul_pow_le_add_pow line 36
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.power_le_of_eventually_pow_le_affine_mul_pow line 41
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_affine_mul_pow line 59
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_mul_pow line 66
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_linear_mul_pow line 72
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.eventually_linear_mul_pow_le_add_pow line 79