OAI/LinearAlgebra/MatrixFields/Construction/JointMaskedAssignment.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.Triple line 23
  2. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.survives line 25
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.eligible line 28
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.mem_eligible_iff line 33
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.assignUseful line 40
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.assignUseful_spec line 45
  7. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.assignments line 61
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseAssignment.assignments_coherent line 75
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointIdealBranches.ideal line 130
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointIdealBranches.branch_eq_delete_ideal line 139
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointIdealBranches.ideal_delete line 172
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointIdealBranches.branch_masked_eq_delete_ideal line 184
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointIdealBranches.masked_source_restriction line 207
  14. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.fiberEquiv line 237
  15. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.positionEquiv line 241
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.positionEquiv_shape line 247
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.positionEquiv_symm_shape line 251
  18. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ClassKey line 257
  19. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ClassPositions line 258
  20. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.RawPairs line 262
  21. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.CanonicalPairs line 263
  22. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.pairEquiv line 266
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.pairEquiv_fiber_left line 292
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.pairEquiv_fiber_right line 298
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.typeWindow_reindex line 303
  26. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.activeLaw line 321
  27. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.activeWidth line 325
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.activeLaw_of_pos line 329
  29. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.rawWindows line 335
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.rawWindows_iff_childWindows line 343
  31. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coarseMask line 378
  32. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coarseWord line 381
  33. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.sourceTensor line 384
  34. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coarseIdeal line 387
  35. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.block line 393
  36. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.canonicalBase line 398
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.product_pack line 404
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coarseIdeal_eq_canonicalBase line 422
  39. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coordinateMatrix line 431
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coordinateMatrix_restrict line 435
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.coarseIdeal_restrict line 446
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.canonicalBase_eq_pairClassProduct line 456
  43. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ideal line 476
  44. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.canonicalIdeal line 483
  45. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.usefulByTriple line 493
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.usefulByTriple_target line 499
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ideal_eq_jointIdeal line 511
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ideal_eq_canonicalIdeal line 534
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalization.ideal_restrict line 543
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.uniqueAssignment_of_unique line 572
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.assignUseful_of_unique line 584
  52. def OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.ambientXCollision line 595
  53. def OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.targetCompatibleCollision line 599
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.eligible_of_no_ambientXCollision line 604
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.not_eligible_iff_ambientXCollision line 616
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.assignUseful_of_no_targetCollision line 628
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.assignment_failure_implies_collision line 642
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.retained_assignment_of_no_collision line 659
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAssignmentLoss.passing_assignment_failure_subset line 675
  60. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.actualTargets line 713
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.coarse_mem_actualTargets line 716
  62. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.xFlag line 720
  63. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.yFlag line 723
  64. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.zFlag line 726
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.actual_survival_iff line 731
  66. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.actualEligible line 739
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.good_mem_actualEligible line 744
  68. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.actualAssignment line 758
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.model_retained_assigned line 764
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.actual_failure_subset_model_missing line 787
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.good_actual_missingFraction_le line 810