OAI/Combinatorics/BalancedRyser/Candidates/CandidateRootCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateExposure.eligibleTupleEquivRootPrescription line 14
  2. theorem OAI.Balanced.CandidateExposure.equivRootPrescription_tuple line 31
  3. theorem OAI.Balanced.CandidateExposure.successfulTupleCount_eq_rootSuccessCount line 37
  4. theorem OAI.Balanced.CandidateExposure.mean_successfulTupleCount line 60
  5. theorem OAI.Balanced.CandidateExposure.rootMean_lower_bound line 67
  6. theorem OAI.Balanced.CandidateExposure.mean_successfulTupleCount_ge line 89
  7. theorem OAI.Balanced.CandidateExposure.integral_successfulTupleCount_original line 100
  8. theorem OAI.Balanced.CandidateExposure.mean_successfulTupleCount_asymptotic line 111