OAI/Combinatorics/BalancedRyser/Incidence/CandidatePointIncidenceMean.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CandidatePointIncidence.probabilitySum_eq_strata line 14
  2. theorem OAI.Balanced.CandidatePointIncidence.probabilitySum_le_of_low line 31
  3. theorem OAI.Balanced.CandidatePointIncidence.point_probabilitySum_le line 58
  4. theorem OAI.Balanced.CandidatePointIncidence.pointLine_probabilitySum_le line 66
  5. def OAI.Balanced.CandidatePointIncidence.pointTest line 74
  6. def OAI.Balanced.CandidatePointIncidence.pointLineTest line 76
  7. theorem OAI.Balanced.CandidatePointIncidence.pointLine_model_event_eq line 80
  8. theorem OAI.Balanced.CandidatePointIncidence.point_model_fixed_count_le line 93
  9. theorem OAI.Balanced.CandidatePointIncidence.pointLine_model_fixed_count_le line 100
  10. theorem OAI.Balanced.CandidatePointIncidence.point_model_moment_le line 108
  11. theorem OAI.Balanced.CandidatePointIncidence.pointLine_model_moment_le line 119