OAI/Combinatorics/BalancedRyser/Incidence/CandidateIncidenceMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CandidateExposure.conditionalProbability_mono line 15
  2. def OAI.Balanced.CandidateExposure.successfulLineHit line 23
  3. theorem OAI.Balanced.CandidateExposure.lineHit_probability_le_success line 27
  4. theorem OAI.Balanced.CandidateExposure.lineHit_probability_fresh_le line 33
  5. theorem OAI.Balanced.CandidateExposure.lineHit_sum_fresh_le line 50
  6. theorem OAI.Balanced.CandidateExposure.lineHit_probabilitySum_le line 70
  7. theorem OAI.Balanced.CandidateExposure.success_sum_two_three_le line 96
  8. theorem OAI.Balanced.CandidateExposure.sum_targets_success_two_three_le line 119
  9. theorem OAI.Balanced.CandidateExposure.sum_targets_success_four_le line 140