OAI/LinearAlgebra/MatrixFields/Extraction/JointMaskedSelection.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot line 20
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot_add_right line 22
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot_sub_right line 25
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot_add_left line 28
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot_sub_left line 31
  6. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointHashing.Sample line 34
  7. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.xHash line 36
  8. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.yHash line 37
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.zHash line 39
  10. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.Survives line 42
  11. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.survivalEquiv line 45
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.hash_relation line 62
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.full_survival_iff line 71
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.survival_card line 89
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.sample_card line 97
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_x_collision_iff line 101
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_y_collision_iff line 115
  18. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.pivot line 130
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.dot_pivot line 133
  20. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.linearSplitEquiv line 137
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.linear_zero_fiber_card line 150
  22. def OAI.MatrixAllFields.MatrixMultiplication.JointHashing.collisionEquiv line 158
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.collision_card_mul line 172
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_x_collision_card_mul line 191
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_y_collision_card_mul line 206
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.survival_fraction line 221
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.collision_fraction line 230
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.small_nat_isUnit line 247
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.coarse_difference_isUnit line 257
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.coarse_words_unit_coordinate line 267
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_z_collision_iff line 277
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.JointHashing.shared_z_collision_card_mul line 301
  33. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.Word line 329
  34. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.Triple line 330
  35. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.HasSupportSum line 334
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.eq_of_shared_xy line 337
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.eq_of_shared_xz line 349
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.eq_of_shared_yz line 361
  39. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.castWord line 373
  40. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.twoUnit line 376
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.twoUnit_coe line 379
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.supportSum_cast line 382
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.shared_z_cast_sum line 390
  44. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.Sample line 402
  45. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.Survives line 404
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.full_survival_iff line 407
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.survival_card line 418
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.shared_x_card_mul line 426
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.shared_y_card_mul line 440
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.shared_z_card_mul line 454
  51. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.SharesSide line 469
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.pair_survival_card_mul line 472
  53. def OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.ownEvent line 482
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.ownEvent_card line 485
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.pair_event_card_mul line 489
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.competitor_union_card_mul_le line 496
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.competitor_union_card_le line 508
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCoarseHashing.pair_survival_fraction line 524
  59. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.neighbors line 556
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.mem_neighbors line 559
  61. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.Bad line 567
  62. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.Good line 571
  63. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.goodEvent line 575
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.mem_goodEvent line 579
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.good_excludes_neighbor line 584
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.good_no_shared_side line 591
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.ownEvent_card_real line 598
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.bad_card_le line 605
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.goodEvent_card_lower line 625
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.goodIncidence_eq line 647
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.exists_selection_of_degree_bound line 656
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.exists_selection_floor line 687
  73. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.hashLevel line 706
  74. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.hashSet line 708
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.hashSet_AP line 711
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinarySelection.eventually_exists_selection line 716
  77. structure OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData line 784
  78. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityCompetitors line 805
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.mem_eligibilityCompetitors line 808
  80. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.variableBad line 817
  81. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityGood line 821
  82. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.Failure line 825
  83. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.Good line 830
  84. def OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.goodEvent line 834
  85. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.mem_goodEvent line 838
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.variableBad_card_le line 843
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityFailure_card_le line 865
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.failure_card_le line 877
  89. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.ownEvent_card_real line 893
  90. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.goodEvent_card_lower line 899
  91. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.goodIncidence_eq line 917
  92. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.good_eligibility line 925
  93. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.good_no_shared_x line 931
  94. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.good_missingFraction_le line 939
  95. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMaskedSelection.OrbitData.exists_selection line 951