OAI/Combinatorics/BalancedRyser/Candidates/CandidatePairCounts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidatePairs.lineTuples line 16
  2. def OAI.Balanced.CandidatePairs.lineCount line 20
  3. def OAI.Balanced.CandidatePairs.targetLine line 22
  4. def OAI.Balanced.CandidatePairs.pairCount line 25
  5. theorem OAI.Balanced.CandidatePairs.lineCount_eq_successfulCodes line 29
  6. theorem OAI.Balanced.CandidatePairs.lineCount_le_card line 45
  7. theorem OAI.Balanced.CandidatePairs.tuplePoint_eq_of_generators line 49
  8. theorem OAI.Balanced.CandidatePairs.successfulInDirection_congr line 58
  9. theorem OAI.Balanced.CandidatePairs.conditional_lineCount_le line 67
  10. theorem OAI.Balanced.CandidatePairs.conditional_partnerCount_le line 75
  11. theorem OAI.Balanced.CandidatePairs.exposed_integral_mul_le line 98
  12. theorem OAI.Balanced.CandidatePairs.integral_success_indicator line 114
  13. theorem OAI.Balanced.CandidatePairs.conditional_first_partner_le line 132
  14. theorem OAI.Balanced.CandidatePairs.integral_sum_pmf line 161
  15. theorem OAI.Balanced.CandidatePairs.conditional_sum_first_partner_le line 169
  16. theorem OAI.Balanced.CandidatePairs.conditional_pairCount_le line 180
  17. def OAI.Balanced.CandidatePairs.firstOverlapPairCount line 195
  18. theorem OAI.Balanced.CandidatePairs.conditional_firstOverlapPairCount_le line 200