OAI/LinearAlgebra/MatrixFields/Histories/HistoryPositions.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.due line 19
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.produced line 26
  3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Carried line 33
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Produced line 34
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.produced_not_resident line 36
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.resident_succ_iff line 45
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stateTransitionForward line 68
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stateTransitionBackward line 80
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stateTransition line 85
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.productionParent line 98
  11. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.DueState line 115
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeToDue line 117
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.dueToActive line 127
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeSourceEquiv line 136
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bSubdivisionPositionEquiv line 151
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.final_state_terminal line 159
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.currentShape line 202
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.currentLength line 209
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.currentPhysicalShape line 215
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.currentShape_spec line 218
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.currentPhysicalShape_total line 237
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positive_iff_no_zero line 241
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.not_positive_has_zero line 258
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.terminal_has_zero line 265
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.terminal_physical_zero line 280
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.final_physical_zero line 285
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.source_shape line 289
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.source_length line 292
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.child_shape line 295
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.child_length line 299
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ResidentStatistic line 322
  32. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 328) line 328
  33. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 331) line 331
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentStatistic line 333
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentLawRat line 341
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentLaw line 350
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentLawRat_nonnegative line 354
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentLawRat_normalized line 363
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentWidth line 376
  40. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.HistoryWord line 383
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentMask line 386
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentMask_zero_population line 396
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentWidth_mono line 403
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.residentMask_mono line 408
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.historyTensor line 420
  46. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stateTensor line 430
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.historyTensor_support_shape line 438
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.historyTensor_initial line 454
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.historyTensor_afterC line 462
  50. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ProducedPositions line 488
  51. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.SplitPositions line 491
  52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.halfPosition line 495
  53. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.unhalfPosition line 501
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.unhalf_halfPosition line 507
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.half_unhalfPosition line 512
  56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.splitToProduced line 517
  57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedToSplit line 536
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedToSplit_splitToProduced line 557
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.splitToProduced_producedToSplit line 580
  60. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedPositionEquiv line 605
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_parent line 613
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_shape line 624
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_length line 640