OAI/Combinatorics/BalancedRyser/Probability/ConditionalMultiplicity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CandidateExposure.exposedLaw_fresh_direction_array line 15
  2. def OAI.Balanced.CandidateExposure.freshMultiplicity line 24
  3. def OAI.Balanced.CandidateExposure.exposedMultiplicity line 28
  4. theorem OAI.Balanced.CandidateExposure.sampledMultiplicity_eq_exposed_add_fresh line 32
  5. theorem OAI.Balanced.CandidateExposure.exposedMultiplicity_le line 48
  6. theorem OAI.Balanced.CandidateExposure.sampledMultiplicity_eq_fixed_add_fresh line 55
  7. theorem OAI.Balanced.CandidateExposure.freshMultiplicity_atom line 72
  8. theorem OAI.Balanced.CandidateExposure.freshMultiplicity_law line 100
  9. theorem OAI.Balanced.CandidateExposure.sampledMultiplicity_conditional_atom line 113
  10. theorem OAI.Balanced.CandidateExposure.sampledMultiplicity_conditional_law line 138