OAI/LinearAlgebra/MatrixMultiplication/Separation/ComplexInitialTargetExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite type counts, hierarchy separation and tensor execution bounds.

  1. def OAI.MatrixMultiplication.Foundation.InitialTargetExecution.scalarOutput line 16
  2. def OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial line 19
  3. theorem OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial_rankBound line 66
  4. theorem OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial_order line 69
  5. theorem OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial_value_ne_zero_iff line 72
  6. theorem OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial_eligible line 80
  7. theorem OAI.MatrixMultiplication.Foundation.InitialTargetExecution.initial_substitution line 87