OAI/Combinatorics/BalancedRyser/Candidates/CandidatePrescribedLine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.CandidatePrescribed.Code line 15
  2. def OAI.Balanced.CandidatePrescribed.exposedLaw line 17
  3. def OAI.Balanced.CandidatePrescribed.Eligible line 22
  4. def OAI.Balanced.CandidatePrescribed.alignmentMass line 25
  5. theorem OAI.Balanced.CandidatePrescribed.alignmentMass_nonneg line 32
  6. theorem OAI.Balanced.CandidatePrescribed.fixedPositions_card_le line 37
  7. theorem OAI.Balanced.CandidatePrescribed.alignmentMass_le line 43
  8. theorem OAI.Balanced.CandidatePrescribed.card_codes_le line 64
  9. theorem OAI.Balanced.CandidatePrescribed.sum_alignmentMass_stratum_le line 94
  10. theorem OAI.Balanced.CandidatePrescribed.codes_stratum_eq_filter line 114
  11. theorem OAI.Balanced.CandidatePrescribed.sum_alignmentMass_le line 121
  12. def OAI.Balanced.CandidatePrescribed.alignedCodes line 143
  13. def OAI.Balanced.CandidatePrescribed.successfulCodes line 147
  14. theorem OAI.Balanced.CandidatePrescribed.alignmentMass_eq_sum line 151
  15. theorem OAI.Balanced.CandidatePrescribed.expected_alignedCodes_eq line 170
  16. theorem OAI.Balanced.CandidatePrescribed.expected_successfulCodes_le line 182
  17. theorem OAI.Balanced.CandidatePrescribed.expected_successfulCodes_le_of_card_le line 198