OAI/LinearAlgebra/MatrixFields/Tensors/CWStageCPlacements.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalProducts.restrict_familyProduct line 19
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalProducts.matrix_restriction_of_history_restrictions line 30
  3. def OAI.MatrixAllFields.MatrixMultiplication.CWStageC.interior line 67
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.interior_injective line 69
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.interior_weight line 75
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.zero_weight line 79
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.last_weight line 81
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.interior_complement line 83
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.coefficient110 line 92
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.coefficient101 line 97
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.coefficient011 line 102
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.coefficient002 line 107
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.branch0 line 110
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.branch1 line 121
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.branch2 line 132
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageC.branch3 line 144
  17. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.SmallRow line 163
  18. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.SmallInner line 165
  19. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.smallRowFintype line 167
  20. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.smallInnerFintype line 171
  21. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.smallRowDecidableEq line 175
  22. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.smallInnerDecidableEq line 179
  23. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.Row line 183
  24. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.Middle line 186
  25. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.Column line 189
  26. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.rowFintype line 192
  27. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.middleFintype line 194
  28. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.columnFintype line 196
  29. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.rowDecidableEq line 198
  30. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.middleDecidableEq line 200
  31. instance OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.columnDecidableEq line 202
  32. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.Word line 205
  33. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.shape line 207
  34. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.source line 209
  35. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.canonicalAtom line 212
  36. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchAtom line 215
  37. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchSource line 220
  38. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.Positions line 228
  39. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.RowWords line 230
  40. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.MiddleWords line 232
  41. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.ColumnWords line 234
  42. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.singleCount line 237
  43. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.crossCount line 238
  44. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.totalCount line 239
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.coefficient_swapXZ line 243
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.coefficient_swapYZ line 249
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.source_zero_apply line 255
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.source_one_apply line 264
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.source_two line 273
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.canonical_pullback line 277
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.canonical_masked_pullback line 290
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchSource_zero_apply line 328
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchSource_one_apply line 333
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.oriented_pullback line 338
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.oriented_masked_pullback line 358
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.oriented_restriction line 378
  57. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.productSource line 392
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.product_restriction line 396
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_positions line 421
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_rowWords line 426
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_middleWords line 434
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_columnWords line 442
  63. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.volume line 450
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.volume_eq line 454
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.volume_pos line 459
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_volume line 463
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.normalized_log_volume line 469
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.totalCount_of_atom_counts line 482
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_volume_of_atom_counts line 493
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.normalized_log_volume_of_atom_counts line 512
  71. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.HistoryRowWords line 523
  72. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.HistoryMiddleWords line 525
  73. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.HistoryColumnWords line 527
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_historyRowWords line 530
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_historyMiddleWords line 537
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.card_historyColumnWords line 544
  77. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.historyVolume line 551
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.historyVolume_eq_prod line 556
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.historyVolume_eq line 561
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_historyVolume line 568
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_historyVolume_of_mass_counts line 575
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.normalized_log_historyVolume_of_mass_counts line 603
  83. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.PopulationHistory line 615
  84. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationSide line 617
  85. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationAtomCounts line 620
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationAtomCounts_mass line 624
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationAtomCounts_parent line 636
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationAtomCounts_total line 644
  89. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_population_historyVolume line 652
  90. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.normalized_log_population_historyVolume line 668
  91. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.populationVolume line 687
  92. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.log_populationVolume line 691
  93. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.normalized_log_populationVolume line 702
  94. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.atomPermutation line 724
  95. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchAtom_transport line 728
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.atomPermutation_single line 734
  97. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchAtom_eq_stageCAtom line 741
  98. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.shape_eq_parent line 745
  99. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.shape_transport line 751
  100. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedBranchSource line 762
  101. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedBranchSource_eq line 770
  102. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placed_branch_restriction line 780
  103. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedProductSource line 797
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placed_product_restriction line 802