OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/Population.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. structure OAI.MatrixMultiplication.JointPopulation.HistoryKey line 17
  2. abbrev OAI.MatrixMultiplication.JointPopulation.Shape line 24
  3. def OAI.MatrixMultiplication.JointPopulation.shapeSide line 26
  4. abbrev OAI.MatrixMultiplication.JointPopulation.Positions line 32
  5. abbrev OAI.MatrixMultiplication.JointPopulation.Target line 33
  6. def OAI.MatrixMultiplication.JointPopulation.canonicalTarget line 35
  7. theorem OAI.MatrixMultiplication.JointPopulation.target_card line 38
  8. theorem OAI.MatrixMultiplication.JointPopulation.target_nonempty line 43
  9. abbrev OAI.MatrixMultiplication.JointPopulation.Position line 45
  10. def OAI.MatrixMultiplication.JointPopulation.triple line 47
  11. theorem OAI.MatrixMultiplication.JointPopulation.triple_injective line 53
  12. def OAI.MatrixMultiplication.JointPopulation.targetSet line 64
  13. theorem OAI.MatrixMultiplication.JointPopulation.targetSet_card line 67
  14. abbrev OAI.MatrixMultiplication.JointPopulation.Class line 72
  15. theorem OAI.MatrixMultiplication.JointPopulation.class_card line 76
  16. theorem OAI.MatrixMultiplication.JointPopulation.symbol_count_pos line 80
  17. theorem OAI.MatrixMultiplication.JointPopulation.triple_support line 86
  18. theorem OAI.MatrixMultiplication.JointPopulation.exists_position_permutation line 94
  19. def OAI.MatrixMultiplication.JointPopulation.sideWord line 104
  20. theorem OAI.MatrixMultiplication.JointPopulation.sideWord_triple line 109
  21. theorem OAI.MatrixMultiplication.JointPopulation.marginal_population_eq line 113
  22. def OAI.MatrixMultiplication.JointPopulation.ambientSet line 120
  23. theorem OAI.MatrixMultiplication.JointPopulation.targetSet_subset_ambient line 126