OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/LossCounts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointLossCounts.card_filter_exists_le line 19
  2. theorem OAI.MatrixMultiplication.JointLossCounts.competitor_union_card_mul_le line 36
  3. def OAI.MatrixMultiplication.JointLossCounts.randomLossCount line 52
  4. def OAI.MatrixMultiplication.JointLossCounts.randomLossFraction line 56
  5. theorem OAI.MatrixMultiplication.JointLossCounts.randomLossFraction_nonneg line 59
  6. theorem OAI.MatrixMultiplication.JointLossCounts.sum_randomLossCount line 63
  7. theorem OAI.MatrixMultiplication.JointLossCounts.sum_randomLossCount_le line 71
  8. theorem OAI.MatrixMultiplication.JointLossCounts.sum_randomLossFraction_le line 89
  9. theorem OAI.MatrixMultiplication.JointLossCounts.conditional_mean_randomLossFraction_le line 102
  10. theorem OAI.MatrixMultiplication.JointLossCounts.card_filter_mul_le_sum line 113
  11. theorem OAI.MatrixMultiplication.JointLossCounts.bad_orbit_card_le line 127
  12. def OAI.MatrixMultiplication.JointLossCounts.targetBad line 146
  13. theorem OAI.MatrixMultiplication.JointLossCounts.targetBad_card_le line 150
  14. theorem OAI.MatrixMultiplication.JointLossCounts.good_card_lower line 201
  15. def OAI.MatrixMultiplication.JointLossCounts.retained line 217
  16. def OAI.MatrixMultiplication.JointLossCounts.deterministicLossFraction line 220
  17. def OAI.MatrixMultiplication.JointLossCounts.missingFraction line 223
  18. theorem OAI.MatrixMultiplication.JointLossCounts.missing_card_eq line 226
  19. theorem OAI.MatrixMultiplication.JointLossCounts.missingFraction_eq line 240
  20. theorem OAI.MatrixMultiplication.JointLossCounts.good_missingFraction_le line 247