OAI/LinearAlgebra/MatrixMultiplication/Separation/ComplexFiniteControl.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite type counts, hierarchy separation and tensor execution bounds.

  1. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.every_path_safe line 22
  2. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.exists_population_preserving_equiv line 37
  3. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.population_product_eq line 51
  4. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.exists_common_bank_multiple line 65
  5. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.exists_exact_rational_tiling line 79
  6. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.target_relation_of_windows line 105
  7. theorem OAI.MatrixMultiplication.Foundation.FiniteControl.synchronized_targets_of_windows line 135