OAI/Computability/DeterministicSum/BilinearForms.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Exact bilinear formulas and recursive simultaneous matrix products.

  1. structure OAI.DeterministicThreeSum.Rectangular.BilinearFormula line 11
  2. def OAI.DeterministicThreeSum.Rectangular.BilinearFormula.coeff line 19
  3. def OAI.DeterministicThreeSum.Rectangular.BilinearFormula.eval line 22
  4. lemma OAI.DeterministicThreeSum.Rectangular.BilinearFormula.eval_eq line 25
  5. def OAI.DeterministicThreeSum.Rectangular.BilinearFormula.evalBilinear line 50
  6. theorem OAI.DeterministicThreeSum.Rectangular.BilinearFormula.evalBilinear_eq line 54
  7. def OAI.DeterministicThreeSum.Rectangular.independentMatrixTensor line 72
  8. lemma OAI.DeterministicThreeSum.Rectangular.independent_evalBilinear line 84
  9. theorem OAI.DeterministicThreeSum.Rectangular.independent_block_products line 95
  10. def OAI.DeterministicThreeSum.Rectangular.reindexIndependent line 104
  11. lemma OAI.DeterministicThreeSum.Rectangular.reindexIndependent_correct line 113
  12. abbrev OAI.DeterministicThreeSum.Rectangular.DigitBox line 136
  13. instance OAI.DeterministicThreeSum.Rectangular.digitBoxZero line 139
  14. instance OAI.DeterministicThreeSum.Rectangular.digitBoxSubsingleton line 141
  15. instance OAI.DeterministicThreeSum.Rectangular.digitBoxFintype line 144
  16. lemma OAI.DeterministicThreeSum.Rectangular.card_DigitBox line 151
  17. def OAI.DeterministicThreeSum.Rectangular.batchCount line 158
  18. lemma OAI.DeterministicThreeSum.Rectangular.batchCount_covers line 160
  19. abbrev OAI.DeterministicThreeSum.Rectangular.FixedFormula line 165
  20. abbrev OAI.DeterministicThreeSum.Rectangular.LeftBatch line 169
  21. abbrev OAI.DeterministicThreeSum.Rectangular.RightBatch line 171
  22. abbrev OAI.DeterministicThreeSum.Rectangular.OutputBatch line 173
  23. def OAI.DeterministicThreeSum.Rectangular.paddedLeft line 176
  24. def OAI.DeterministicThreeSum.Rectangular.paddedRight line 182
  25. def OAI.DeterministicThreeSum.Rectangular.childLeft line 188
  26. def OAI.DeterministicThreeSum.Rectangular.childRight line 193
  27. def OAI.DeterministicThreeSum.Rectangular.parentBatch line 198
  28. def OAI.DeterministicThreeSum.Rectangular.parentSlot line 202
  29. lemma OAI.DeterministicThreeSum.Rectangular.parent_index line 204
  30. def OAI.DeterministicThreeSum.Rectangular.combineChildren line 208
  31. lemma OAI.DeterministicThreeSum.Rectangular.paddedLeft_parent line 214
  32. lemma OAI.DeterministicThreeSum.Rectangular.paddedRight_parent line 224
  33. lemma OAI.DeterministicThreeSum.Rectangular.combineChildren_correct line 234
  34. def OAI.DeterministicThreeSum.Rectangular.multiplyBatch line 254
  35. theorem OAI.DeterministicThreeSum.Rectangular.multiplyBatch_correct line 260