OAI/Combinatorics/BalancedRyser/Candidates/CandidateGeneratorPairModel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.CandidateGeneratorPair.patternModel line 17
  2. theorem OAI.Balanced.CandidateGeneratorPair.support_card line 30
  3. def OAI.Balanced.CandidateGeneratorPair.count line 34
  4. theorem OAI.Balanced.CandidateGeneratorPair.patternModel_count line 38
  5. theorem OAI.Balanced.CandidateGeneratorPair.patternModel_measure line 54
  6. theorem OAI.Balanced.CandidateGeneratorPair.fixedExpectation_exposed line 58
  7. def OAI.Balanced.CandidateGeneratorPair.probabilitySum line 64
  8. theorem OAI.Balanced.CandidateGeneratorPair.count_eq_sum_eligible line 68
  9. theorem OAI.Balanced.CandidateGeneratorPair.integral_count line 97
  10. theorem OAI.Balanced.CandidateGeneratorPair.card_le_exposed_indices line 106
  11. theorem OAI.Balanced.CandidateGeneratorPair.probabilitySum_le_exposure_strata line 116