OAI/LinearAlgebra/MatrixMultiplication/Separation/ComplexLabelHierarchySeparation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Finite type counts, hierarchy separation and tensor execution bounds.

  1. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.populationCoordinateEquiv line 23
  2. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.tensor_transport line 30
  3. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.bankTensor_population_reindex line 39
  4. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.bankTensor_population_rankAtMost line 54
  5. abbrev OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.BankOccurrences line 64
  6. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_bank_product line 67
  7. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_pairing_card line 73
  8. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.canonical_bank_rankAtMost line 79
  9. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.occurrence_product line 92
  10. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_population_product line 99
  11. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_population_bank_equiv line 108
  12. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.prefix_separation_identity line 130
  13. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.prefix_separation_rankAtMost line 154
  14. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.separated_coefficient line 171
  15. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.deterministic_separation_identity line 177
  16. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.separated_prefix_synchronized line 186
  17. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolEnumeration line 210
  18. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode line 214
  19. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode_decode line 221
  20. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolCode_agree line 230
  21. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryCost line 243
  22. abbrev OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.PoolAuxiliaryGroup line 246
  23. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryTensor line 249
  24. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.poolAuxiliaryTensor_rankAtMost line 254
  25. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_mem_restrictionOrbit line 267
  26. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_raw_prefix_synchronized line 295
  27. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_rankAtMost line 320
  28. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_borderRankAtMost line 355
  29. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_optimized_pullback line 395
  30. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.exact_pool_optimized_mem_restrictionOrbit line 435
  31. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.shared_branch_rankAtMost line 460
  32. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.AuxiliaryCoordinates line 487
  33. instance OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryCoordinatesFintype line 491
  34. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryTensor line 499
  35. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.sourceCoordinate line 505
  36. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryCoordinate line 510
  37. def OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor line 515
  38. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_eq_shared_bank line 525
  39. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.auxiliaryTensor_rankAtMost line 549
  40. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_rankAtMost line 563
  41. theorem OAI.MatrixMultiplication.Foundation.LabelHierarchySeparation.stageTensor_borderRankAtMost line 576