OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/FiniteFamily.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. structure OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap line 20
  2. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.identity line 36
  3. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.delete line 44
  4. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.product line 54
  5. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.comp line 65
  6. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.withSource line 73
  7. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.ofExists line 80
  8. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.parallelCopies line 86
  9. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.directSum line 97
  10. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.selectBranches line 109
  11. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.unflatten line 120
  12. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.flatten line 132
  13. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.replicationProduct line 144
  14. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.extract line 157
  15. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.repairBranches line 166
  16. structure OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution line 177
  17. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.initial line 194
  18. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.restrict line 207
  19. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.replicate line 213
  20. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.step line 221
  21. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.stepOnLeft line 227
  22. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.branchOperation line 237
  23. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.branchOperation_copies line 251
  24. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.step_copies line 264
  25. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractAndRepair line 272
  26. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractAndRepair_copies line 285
  27. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractSelectedAndRepair line 297
  28. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractSelectedAndRepair_copies line 315
  29. def OAI.MatrixMultiplication.AllFieldFiniteFamily.run line 341
  30. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.run_copies line 345
  31. abbrev OAI.MatrixMultiplication.AllFieldFiniteFamily.cwSource line 360
  32. def OAI.MatrixMultiplication.AllFieldFiniteFamily.startCW line 363
  33. def OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.toWitness line 367
  34. theorem OAI.MatrixMultiplication.AllFieldFiniteFamily.Execution.toWitness_rankBound line 374