OAI/Combinatorics/BalancedRyser/Incidence/CandidateIncidenceModel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.CandidateIncidence.Test line 18
  2. def OAI.Balanced.CandidateIncidence.event line 20
  3. abbrev OAI.Balanced.CandidateIncidence.model line 24
  4. abbrev OAI.Balanced.CandidateIncidence.allModel line 37
  5. theorem OAI.Balanced.CandidateIncidence.model_support_card line 50
  6. theorem OAI.Balanced.CandidateIncidence.allModel_support_card line 53
  7. def OAI.Balanced.CandidateIncidence.tupleCount line 56
  8. theorem OAI.Balanced.CandidateIncidence.model_count line 60
  9. theorem OAI.Balanced.CandidateIncidence.allModel_count line 83
  10. theorem OAI.Balanced.CandidateIncidence.model_measure line 90
  11. theorem OAI.Balanced.CandidateIncidence.allModel_measure line 93
  12. theorem OAI.Balanced.CandidateIncidence.model_fixedExpectation line 96
  13. theorem OAI.Balanced.CandidateIncidence.allModel_fixedExpectation line 101
  14. theorem OAI.Balanced.CandidateIncidence.model_fixed_count line 106
  15. theorem OAI.Balanced.CandidateIncidence.allModel_fixed_count line 117
  16. def OAI.Balanced.CandidateIncidence.overlapTest line 131
  17. theorem OAI.Balanced.CandidateIncidence.model_overlapCount line 134
  18. theorem OAI.Balanced.CandidateIncidence.allModel_overlapCount line 145
  19. theorem OAI.Balanced.CandidateIncidence.allModel_fixed_overlapCount line 156
  20. def OAI.Balanced.CandidateIncidence.lineHitTest line 169
  21. theorem OAI.Balanced.CandidateIncidence.lineHit_model_fixed_count_le line 171
  22. theorem OAI.Balanced.CandidateIncidence.lineHit_model_moment_le line 178