OAI/Combinatorics/RamseyFive/Probability/MeasurePreservingSplitSchedule.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.PoissonScore.measurePreserving_split_schedule line 14
  2. lemma OAI.SharpRamseyFive.PoissonScore.integral_split_schedule line 30
  3. lemma OAI.SharpRamseyFive.PoissonScore.integral_split_schedule_le line 50
  4. def OAI.SharpRamseyFive.ScoreAcceptance.empty line 73
  5. lemma OAI.SharpRamseyFive.ScoreAcceptance.empty_union line 76
  6. def OAI.SharpRamseyFive.ScoreAcceptance.factor line 80
  7. lemma OAI.SharpRamseyFive.ScoreAcceptance.abs_factor_le_one line 83
  8. lemma OAI.SharpRamseyFive.ScoreAcceptance.abs_factor_of_nonempty line 88
  9. def OAI.SharpRamseyFive.ScoreAcceptance.term line 92
  10. def OAI.SharpRamseyFive.ScoreAcceptance.allEmpty line 95
  11. lemma OAI.SharpRamseyFive.ScoreAcceptance.own_split line 98
  12. lemma OAI.SharpRamseyFive.ScoreAcceptance.term_empty line 111
  13. lemma OAI.SharpRamseyFive.ScoreAcceptance.term_nonempty line 123
  14. def OAI.SharpRamseyFive.ScoreAcceptance.emptyFamily line 144
  15. theorem OAI.SharpRamseyFive.ScoreAcceptance.exceptional_error line 150
  16. lemma OAI.SharpRamseyFive.ScoreAcceptance.training_separation line 173
  17. lemma OAI.SharpRamseyFive.ScoreAcceptance.ambient_separation line 182
  18. def OAI.SharpRamseyFive.ScoreAcceptance.accepted line 193
  19. lemma OAI.SharpRamseyFive.ScoreAcceptance.capture line 196
  20. lemma OAI.SharpRamseyFive.ScoreAcceptance.size_bound line 209