OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/OrdinarySelection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointOrdinarySelection.neighbors line 19
  2. theorem OAI.MatrixMultiplication.JointOrdinarySelection.mem_neighbors line 22
  3. def OAI.MatrixMultiplication.JointOrdinarySelection.Bad line 30
  4. def OAI.MatrixMultiplication.JointOrdinarySelection.Good line 34
  5. def OAI.MatrixMultiplication.JointOrdinarySelection.goodEvent line 38
  6. theorem OAI.MatrixMultiplication.JointOrdinarySelection.mem_goodEvent line 42
  7. theorem OAI.MatrixMultiplication.JointOrdinarySelection.good_excludes_neighbor line 47
  8. theorem OAI.MatrixMultiplication.JointOrdinarySelection.good_no_shared_side line 54
  9. theorem OAI.MatrixMultiplication.JointOrdinarySelection.ownEvent_card_real line 61
  10. theorem OAI.MatrixMultiplication.JointOrdinarySelection.bad_card_le line 77
  11. theorem OAI.MatrixMultiplication.JointOrdinarySelection.goodEvent_card_lower line 97
  12. theorem OAI.MatrixMultiplication.JointOrdinarySelection.goodIncidence_eq line 119
  13. theorem OAI.MatrixMultiplication.JointOrdinarySelection.exists_selection_of_degree_bound line 128
  14. theorem OAI.MatrixMultiplication.JointOrdinarySelection.exists_selection_floor line 159
  15. def OAI.MatrixMultiplication.JointOrdinarySelection.hashLevel line 178
  16. def OAI.MatrixMultiplication.JointOrdinarySelection.hashSet line 180
  17. theorem OAI.MatrixMultiplication.JointOrdinarySelection.hashSet_AP line 183
  18. theorem OAI.MatrixMultiplication.JointOrdinarySelection.eventually_exists_selection line 188