OAI/Combinatorics/BalancedRyser/Candidates/CandidateTwoLineMoments.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateIncidenceSums.tupleIncidenceSum line 17
  2. theorem OAI.Balanced.CandidateIncidenceSums.rootIncidenceSum_eq_tupleIncidenceSum line 22
  3. theorem OAI.Balanced.CandidateIncidenceSums.tupleIncidenceSum_le_success line 42
  4. theorem OAI.Balanced.CandidateIncidenceSums.allModel_fixed_count_eq_sum_strata line 52
  5. def OAI.Balanced.CandidateIncidenceSums.twoLineTest line 74
  6. theorem OAI.Balanced.CandidateIncidenceSums.twoLine_stratum_le line 76
  7. theorem OAI.Balanced.CandidateIncidenceSums.twoLine_model_fixed_count_le line 104
  8. def OAI.Balanced.CandidateIncidenceSums.twoLineInitial line 119
  9. def OAI.Balanced.CandidateIncidenceSums.twoLineAllowed line 121
  10. theorem OAI.Balanced.CandidateIncidenceSums.twoLineInitial_card_le line 125
  11. theorem OAI.Balanced.CandidateIncidenceSums.twoLineAllowed_depends line 131
  12. abbrev OAI.Balanced.CandidateIncidenceSums.twoLineModel line 138
  13. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_measure line 142
  14. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_count line 145
  15. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_support_card line 151
  16. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_fixed_initial_count_le line 158
  17. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_fixed_count_le line 181
  18. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_fixed_moment_le line 203
  19. theorem OAI.Balanced.CandidateIncidenceSums.twoLineModel_moment_le line 213