OAI/Combinatorics/RamseyFive/Probability/Aggregate.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.PoissonScore.poisson_zero line 14
  2. lemma OAI.SharpRamseyFive.PoissonScore.hasLaw_coordinate line 23
  3. lemma OAI.SharpRamseyFive.PoissonScore.coordinate_independent line 28
  4. lemma OAI.SharpRamseyFive.PoissonScore.hasLaw_sum line 32
  5. def OAI.SharpRamseyFive.PoissonScore.aggregate line 52
  6. def OAI.SharpRamseyFive.PoissonScore.aggregateRate line 55
  7. theorem OAI.SharpRamseyFive.PoissonScore.measurePreserving_aggregate line 58
  8. lemma OAI.SharpRamseyFive.PoissonScore.emptyIndicator_aggregate line 70
  9. lemma OAI.SharpRamseyFive.PoissonScore.measurePreserving_schedule_aggregate line 95
  10. lemma OAI.SharpRamseyFive.PoissonScore.scoreTerm_aggregate line 101
  11. lemma OAI.SharpRamseyFive.PoissonScore.integral_split_counts line 109
  12. lemma OAI.SharpRamseyFive.PoissonScore.integral_split_counts_le line 130
  13. lemma OAI.SharpRamseyFive.ValidationMoment.add_power_bound line 153
  14. theorem OAI.SharpRamseyFive.ValidationMoment.finite_second_sum line 159
  15. lemma OAI.SharpRamseyFive.ValidationMoment.mass_scale line 216
  16. lemma OAI.SharpRamseyFive.ValidationMoment.diagonal_one_batch line 220
  17. theorem OAI.SharpRamseyFive.ValidationMoment.poisson_validation_second line 235