OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ShapeEncoding.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldHistory.shapeTotal line 14
  2. def OAI.MatrixMultiplication.AllFieldHistory.ShapeBounded line 16
  3. def OAI.MatrixMultiplication.AllFieldHistory.encodeShape line 18
  4. def OAI.MatrixMultiplication.AllFieldHistory.decodeShape line 22
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.decode_encodeShape line 25
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.encodeShape_side line 30
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.decodeShape_bounded line 34
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.encode_decodeShape line 40
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.encodeShape_inj line 47
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.encodeShape_injective line 51
  11. theorem OAI.MatrixMultiplication.AllFieldHistory.encodeShape_total line 57
  12. def OAI.MatrixMultiplication.AllFieldHistory.physicalShape line 61
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_source line 64
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_bounded line 68
  15. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_le line 72
  16. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_complement line 76
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_total line 80
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalShape_injective line 85
  19. def OAI.MatrixMultiplication.AllFieldHistory.encodePhysicalShape line 91
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.decode_encodePhysicalShape line 94
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_side line 99
  22. theorem OAI.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_inj line 104
  23. theorem OAI.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_total line 109
  24. theorem OAI.MatrixMultiplication.AllFieldHistory.mem_shapes_total line 115
  25. theorem OAI.MatrixMultiplication.AllFieldHistory.coordinate_le_total line 121
  26. theorem OAI.MatrixMultiplication.AllFieldHistory.mem_shapes_bound line 130
  27. theorem OAI.MatrixMultiplication.AllFieldHistory.mem_shapes_bounded line 133
  28. theorem OAI.MatrixMultiplication.AllFieldHistory.below_mem_shapes line 136
  29. theorem OAI.MatrixMultiplication.AllFieldHistory.below_total line 139
  30. theorem OAI.MatrixMultiplication.AllFieldHistory.below_le line 142
  31. theorem OAI.MatrixMultiplication.AllFieldHistory.below_bounded line 152
  32. theorem OAI.MatrixMultiplication.AllFieldHistory.complement_bounded line 155
  33. theorem OAI.MatrixMultiplication.AllFieldHistory.complement_total line 158
  34. theorem OAI.MatrixMultiplication.AllFieldHistory.root_shape_spec line 166
  35. theorem OAI.MatrixMultiplication.AllFieldHistory.root_shapes_nodup line 171
  36. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_below_nodup line 173
  37. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_below_nodup line 176
  38. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_get_injective line 179
  39. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_get_injective line 183
  40. theorem OAI.MatrixMultiplication.AllFieldHistory.positiveInitial_shape_spec line 187
  41. theorem OAI.MatrixMultiplication.AllFieldHistory.positiveSecond_shape_spec line 191
  42. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_shape_spec line 196
  43. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_complement_spec line 201
  44. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_shape_spec line 207
  45. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_complement_spec line 212
  46. theorem OAI.MatrixMultiplication.AllFieldHistory.stageC_shape_spec line 218
  47. theorem OAI.MatrixMultiplication.AllFieldHistory.stageC_complement_spec line 224