OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/MaskedSelection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. structure OAI.MatrixMultiplication.JointMaskedSelection.OrbitData line 19
  2. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityCompetitors line 40
  3. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.mem_eligibilityCompetitors line 43
  4. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.variableBad line 52
  5. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityGood line 56
  6. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.Failure line 60
  7. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.Good line 65
  8. def OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.goodEvent line 69
  9. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.mem_goodEvent line 73
  10. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.variableBad_card_le line 78
  11. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.eligibilityFailure_card_le line 100
  12. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.failure_card_le line 112
  13. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.ownEvent_card_real line 128
  14. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.goodEvent_card_lower line 145
  15. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.goodIncidence_eq line 163
  16. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.good_eligibility line 171
  17. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.good_no_shared_x line 177
  18. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.good_missingFraction_le line 185
  19. theorem OAI.MatrixMultiplication.JointMaskedSelection.OrbitData.exists_selection line 197