OAI/LinearAlgebra/MatrixFields/Parameters/JointPopulationMixedCompatibility.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.ClassKey line 26
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.ClassPos line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.classCounts line 31
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.FixedSideTargets line 34
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.candidateEquiv line 37
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.candidateEquiv_apply line 72
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.classCounts_size line 77
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.fixedSideTargets_card line 87
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.shapeStatisticCount line 94
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.scaled_count_window line 98
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.shape_count_window_of_typeWindow line 108
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.jointCount_le_population line 131
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.class_jointCount_eq line 142
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.class_jointCount_zero line 175
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.side_compatibility_iff_class_counts line 189
  16. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.statisticWord line 229
  17. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.statisticCounts line 234
  18. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.statisticElement line 239
  19. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.Compatible line 248
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatible_of_designated_windows line 260
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatible_iff_kernel line 277
  22. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleTargetCount line 293
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleTargetCount_eq_kernel line 299
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleTarget_incidence line 312
  25. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleByTriple line 330
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleByTriple_target line 338
  27. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse line 352
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_target line 361
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_shares_side line 373
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.compatibleWithCoarse_target_count line 386
  31. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.designatedYLeft line 404
  32. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.designatedYRight line 407
  33. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.designatedZLeft line 411
  34. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationCompatibility.designatedZRight line 414
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationMixedNonzero.class_half_products_nonzero line 437
  36. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationMixedCompatibility.sharingDesignated line 512
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationMixedCompatibility.source_implies_compatibleY line 549
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationMixedCompatibility.source_implies_compatibleZ line 585