OAI/LinearAlgebra/MatrixMultiplication/Rectangular/RateLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix multiplication algorithms and their asymptotic exponents.

  1. theorem OAI.MatrixMultiplication.RectangularRateLimit.eventually_two_le_of_positive_log_rate line 14
  2. theorem OAI.MatrixMultiplication.RectangularRateLimit.eventually_aspect_of_rate_gap line 25
  3. theorem OAI.MatrixMultiplication.RectangularRateLimit.rate_inequality_of_log_bounds line 43
  4. theorem OAI.MatrixMultiplication.RectangularRateLimit.exponent_le_of_finite_asi line 60