OAI/Combinatorics/BalancedRyser/Candidates/CandidateFirstMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateExposure.eligibleTuples line 13
  2. def OAI.Balanced.CandidateExposure.tuplesWithExposure line 16
  3. theorem OAI.Balanced.CandidateExposure.card_tupleCodesWithOldCount_le_bounded line 20
  4. theorem OAI.Balanced.CandidateExposure.card_tuplesWithExposure_le line 43
  5. theorem OAI.Balanced.CandidateExposure.counting_alignment_scale line 60
  6. theorem OAI.Balanced.CandidateExposure.success_sum_withExposure_le line 65
  7. def OAI.Balanced.CandidateExposure.successProbabilitySum line 89
  8. def OAI.Balanced.CandidateExposure.overlapProbabilitySum line 93
  9. theorem OAI.Balanced.CandidateExposure.successProbabilitySum_le line 98
  10. theorem OAI.Balanced.CandidateExposure.overlapProbabilitySum_le line 127