OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/PopulationCompatibility.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointPopulationCompatibility.ClassKey line 22
  2. abbrev OAI.MatrixMultiplication.JointPopulationCompatibility.ClassPos line 24
  3. def OAI.MatrixMultiplication.JointPopulationCompatibility.classCounts line 27
  4. abbrev OAI.MatrixMultiplication.JointPopulationCompatibility.FixedSideTargets line 30
  5. def OAI.MatrixMultiplication.JointPopulationCompatibility.candidateEquiv line 33
  6. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.candidateEquiv_apply line 68
  7. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.classCounts_size line 73
  8. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.fixedSideTargets_card line 83
  9. def OAI.MatrixMultiplication.JointPopulationCompatibility.shapeStatisticCount line 90
  10. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.scaled_count_window line 94
  11. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.shape_count_window_of_typeWindow line 104
  12. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.jointCount_le_population line 127
  13. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.class_jointCount_eq line 138
  14. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.class_jointCount_zero line 171
  15. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.side_compatibility_iff_class_counts line 185
  16. def OAI.MatrixMultiplication.JointPopulationCompatibility.statisticWord line 225
  17. def OAI.MatrixMultiplication.JointPopulationCompatibility.statisticCounts line 230
  18. def OAI.MatrixMultiplication.JointPopulationCompatibility.statisticElement line 235
  19. def OAI.MatrixMultiplication.JointPopulationCompatibility.Compatible line 244
  20. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatible_of_designated_windows line 256
  21. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatible_iff_kernel line 273
  22. def OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleTargetCount line 289
  23. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleTargetCount_eq_kernel line 295
  24. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleTarget_incidence line 308
  25. def OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleByTriple line 326
  26. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleByTriple_target line 334
  27. def OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse line 348
  28. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_target line 357
  29. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_shares_side line 369
  30. theorem OAI.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_target_count line 382
  31. def OAI.MatrixMultiplication.JointPopulationCompatibility.designatedYLeft line 400
  32. def OAI.MatrixMultiplication.JointPopulationCompatibility.designatedYRight line 403
  33. def OAI.MatrixMultiplication.JointPopulationCompatibility.designatedZLeft line 407
  34. def OAI.MatrixMultiplication.JointPopulationCompatibility.designatedZRight line 410