OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/TerminalStatisticLaws.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.AZero line 16
  2. abbrev OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.BZero line 19
  3. abbrev OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.TerminalZero line 22
  4. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_mem_shapes line 26
  5. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_not_positive line 29
  6. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_mem_zeroSecond line 33
  7. def OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bParent line 36
  8. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bParent_mem_positiveSecond line 38
  9. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_mem_shapes line 41
  10. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_mem_below line 44
  11. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_max_lt_five line 47
  12. def OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bWeight line 52
  13. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.bWeight_val line 55
  14. def OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.Slot line 58
  15. instance OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.(instance at line 62) line 62
  16. def OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.history line 65
  17. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_inl line 69
  18. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_inr line 72
  19. def OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.law line 75
  20. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_inl line 79
  21. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_inr line 82
  22. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.statisticLaw_nonnegative line 86
  23. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.statisticLaw_total line 92
  24. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_nonneg line 96
  25. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_total line 101
  26. theorem OAI.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_amount_pos line 106