OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexFactorialLogBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.factorialLogRemainder line 15
  2. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_eq line 18
  3. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_zero line 22
  4. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_stirling line 25
  5. theorem OAI.MatrixMultiplication.Foundation.tendsto_factorialLogRemainder_div line 36
  6. theorem OAI.MatrixMultiplication.Foundation.tendsto_factorialLogRemainder_mul_div line 61
  7. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_succ line 80
  8. theorem OAI.MatrixMultiplication.Foundation.nat_mul_log_increment_le_one line 89
  9. theorem OAI.MatrixMultiplication.Foundation.one_le_succ_mul_log_increment line 103
  10. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_nonneg line 116
  11. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_le_one_add_log_pos line 124
  12. theorem OAI.MatrixMultiplication.Foundation.factorialLogRemainder_le_one_add_log line 134
  13. theorem OAI.MatrixMultiplication.Foundation.abs_factorialLogRemainder_le line 145