OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CoarseHashing.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointCoarseHashing.Word line 14
  2. abbrev OAI.MatrixMultiplication.JointCoarseHashing.Triple line 15
  3. def OAI.MatrixMultiplication.JointCoarseHashing.HasSupportSum line 19
  4. theorem OAI.MatrixMultiplication.JointCoarseHashing.eq_of_shared_xy line 22
  5. theorem OAI.MatrixMultiplication.JointCoarseHashing.eq_of_shared_xz line 34
  6. theorem OAI.MatrixMultiplication.JointCoarseHashing.eq_of_shared_yz line 46
  7. def OAI.MatrixMultiplication.JointCoarseHashing.castWord line 58
  8. def OAI.MatrixMultiplication.JointCoarseHashing.twoUnit line 61
  9. theorem OAI.MatrixMultiplication.JointCoarseHashing.twoUnit_coe line 64
  10. theorem OAI.MatrixMultiplication.JointCoarseHashing.supportSum_cast line 67
  11. theorem OAI.MatrixMultiplication.JointCoarseHashing.shared_z_cast_sum line 75
  12. abbrev OAI.MatrixMultiplication.JointCoarseHashing.Sample line 87
  13. def OAI.MatrixMultiplication.JointCoarseHashing.Survives line 89
  14. theorem OAI.MatrixMultiplication.JointCoarseHashing.full_survival_iff line 92
  15. theorem OAI.MatrixMultiplication.JointCoarseHashing.survival_card line 103
  16. theorem OAI.MatrixMultiplication.JointCoarseHashing.shared_x_card_mul line 111
  17. theorem OAI.MatrixMultiplication.JointCoarseHashing.shared_y_card_mul line 126
  18. theorem OAI.MatrixMultiplication.JointCoarseHashing.shared_z_card_mul line 141
  19. def OAI.MatrixMultiplication.JointCoarseHashing.SharesSide line 157
  20. theorem OAI.MatrixMultiplication.JointCoarseHashing.pair_survival_card_mul line 160
  21. def OAI.MatrixMultiplication.JointCoarseHashing.ownEvent line 170
  22. theorem OAI.MatrixMultiplication.JointCoarseHashing.ownEvent_card line 173
  23. theorem OAI.MatrixMultiplication.JointCoarseHashing.pair_event_card_mul line 177
  24. theorem OAI.MatrixMultiplication.JointCoarseHashing.competitor_union_card_mul_le line 184
  25. theorem OAI.MatrixMultiplication.JointCoarseHashing.competitor_union_card_le line 196
  26. theorem OAI.MatrixMultiplication.JointCoarseHashing.pair_survival_fraction line 212