OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/Hashing.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointHashing.dot line 21
  2. theorem OAI.MatrixMultiplication.JointHashing.dot_add_right line 23
  3. theorem OAI.MatrixMultiplication.JointHashing.dot_sub_right line 26
  4. theorem OAI.MatrixMultiplication.JointHashing.dot_add_left line 29
  5. theorem OAI.MatrixMultiplication.JointHashing.dot_sub_left line 32
  6. abbrev OAI.MatrixMultiplication.JointHashing.Sample line 35
  7. def OAI.MatrixMultiplication.JointHashing.xHash line 37
  8. def OAI.MatrixMultiplication.JointHashing.yHash line 38
  9. def OAI.MatrixMultiplication.JointHashing.zHash line 40
  10. def OAI.MatrixMultiplication.JointHashing.Survives line 43
  11. def OAI.MatrixMultiplication.JointHashing.survivalEquiv line 46
  12. theorem OAI.MatrixMultiplication.JointHashing.hash_relation line 63
  13. theorem OAI.MatrixMultiplication.JointHashing.full_survival_iff line 72
  14. theorem OAI.MatrixMultiplication.JointHashing.survival_card line 90
  15. theorem OAI.MatrixMultiplication.JointHashing.sample_card line 98
  16. theorem OAI.MatrixMultiplication.JointHashing.shared_x_collision_iff line 102
  17. theorem OAI.MatrixMultiplication.JointHashing.shared_y_collision_iff line 116
  18. def OAI.MatrixMultiplication.JointHashing.pivot line 131
  19. theorem OAI.MatrixMultiplication.JointHashing.dot_pivot line 134
  20. def OAI.MatrixMultiplication.JointHashing.linearSplitEquiv line 138
  21. theorem OAI.MatrixMultiplication.JointHashing.linear_zero_fiber_card line 151
  22. def OAI.MatrixMultiplication.JointHashing.collisionEquiv line 159
  23. theorem OAI.MatrixMultiplication.JointHashing.collision_card_mul line 173
  24. theorem OAI.MatrixMultiplication.JointHashing.shared_x_collision_card_mul line 192
  25. theorem OAI.MatrixMultiplication.JointHashing.shared_y_collision_card_mul line 207
  26. theorem OAI.MatrixMultiplication.JointHashing.survival_fraction line 222
  27. theorem OAI.MatrixMultiplication.JointHashing.collision_fraction line 231
  28. theorem OAI.MatrixMultiplication.JointHashing.small_nat_isUnit line 248
  29. theorem OAI.MatrixMultiplication.JointHashing.coarse_difference_isUnit line 258
  30. theorem OAI.MatrixMultiplication.JointHashing.coarse_words_unit_coordinate line 268
  31. theorem OAI.MatrixMultiplication.JointHashing.shared_z_collision_iff line 278
  32. theorem OAI.MatrixMultiplication.JointHashing.shared_z_collision_card_mul line 302