OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ScheduledYield.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldScheduledYield.workCapacity line 21
  2. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.workCapacity_stageC line 24
  3. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.sum_interiorPairs line 31
  4. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.stageCSourceCapacity_native line 45
  5. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.active_native_capacity line 63
  6. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.physical_order_native_capacity line 71
  7. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.order_capacity_eq_physical line 78
  8. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.order_capacity_eq_native line 98
  9. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.order_dilation_capacity line 106
  10. def OAI.MatrixMultiplication.AllFieldScheduledYield.physicalYield line 117
  11. def OAI.MatrixMultiplication.AllFieldScheduledYield.scheduledYield line 122
  12. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.physicalYield_eq_scheduled line 126
  13. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.balanced_scheduledYield line 133
  14. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.nativeLC_tendsto line 138
  15. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.tickCapacity_tendsto line 145
  16. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.scheduledYield_tendsto line 160
  17. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.physicalYield_tendsto_balanced line 171
  18. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.exists_balanced_allocation_sequence line 180
  19. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.exists_physicalYield_limit line 204
  20. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.initial_capacity line 213
  21. theorem OAI.MatrixMultiplication.AllFieldScheduledYield.initial_dilation_capacity line 221