OAI/LinearAlgebra/MatrixFields/Tensors/CWStageCStatistics.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.ChildPair line 17
  2. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.joinChildren line 19
  3. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.splitChildren line 20
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.joinChildren_zero line 22
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.joinChildren_one line 23
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.join_split_children line 25
  7. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.siteTensor line 29
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.siteTensor_support line 35
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.siteProduct_side_weights line 42
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.siteTensor_eq_shapeTensor line 61
  11. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.childProduct line 69
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchAtom_le_shape line 74
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.weight_joinChildren line 78
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.strand_joinChildren line 83
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.masked_eq_childProduct line 88
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.childProduct_split line 114
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.childProduct_pullback line 122
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.childProduct_restriction line 136
  19. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProduct line 150
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProduct_eq line 154
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProduct_eq_stageC line 168
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProduct_side_weights line 178
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProduct_restriction line 187
  24. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProducts line 204
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProducts_side_weights line 210
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProducts_restriction line 223
  27. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.ChildWords line 252
  28. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.singletonChildWords line 254
  29. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.collapseChildWords line 257
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.singleton_collapse_childWords line 259
  31. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProduct line 263
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProduct_eq_stageC line 270
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProduct_pullback line 282
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProduct_restriction line 295
  35. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProducts line 313
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProducts_collapse line 320
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProducts_restriction line 333
  38. def OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.branchStatistic line 362
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.twoStatistic_of_side_weights line 365
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placed_twoStatistic_of_side_weights line 376
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.wordPopulation_of_branchStatistic line 384
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.empiricalLaw_eq_littleLaw line 400
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.typeWindow_of_placed_side_weights line 436
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedChildProducts_support_typeWindow line 458
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStageCProducts.placedShapeChildProducts_support_typeWindow line 474