OAI/Combinatorics/FiniteCircle/Partitions.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FiniteCircle.FiniteLaw line 12
  2. def OAI.FiniteCircle.FiniteLaw.expect line 20
  3. def OAI.FiniteCircle.FiniteLaw.event line 22
  4. theorem OAI.FiniteCircle.FiniteLaw.event_eq_expect line 26
  5. theorem OAI.FiniteCircle.FiniteLaw.expect_nonneg line 34
  6. theorem OAI.FiniteCircle.FiniteLaw.expect_mono line 37
  7. theorem OAI.FiniteCircle.FiniteLaw.expect_const line 41
  8. theorem OAI.FiniteCircle.FiniteLaw.expect_add line 44
  9. theorem OAI.FiniteCircle.FiniteLaw.expect_sub line 48
  10. theorem OAI.FiniteCircle.FiniteLaw.expect_smul line 52
  11. theorem OAI.FiniteCircle.FiniteLaw.expect_sum line 56
  12. theorem OAI.FiniteCircle.FiniteLaw.event_nonneg line 61
  13. theorem OAI.FiniteCircle.FiniteLaw.event_mono line 67
  14. theorem OAI.FiniteCircle.FiniteLaw.event_true line 76
  15. theorem OAI.FiniteCircle.FiniteLaw.event_false line 79
  16. theorem OAI.FiniteCircle.FiniteLaw.event_le_one line 81
  17. theorem OAI.FiniteCircle.FiniteLaw.event_compl line 84
  18. theorem OAI.FiniteCircle.FiniteLaw.event_exists_le_sum line 94
  19. def OAI.FiniteCircle.selectionWeight line 110
  20. def OAI.FiniteCircle.selectionLabel line 113
  21. theorem OAI.FiniteCircle.selectionWeight_nonneg line 116
  22. theorem OAI.FiniteCircle.selectionWeight_total line 124
  23. theorem OAI.FiniteCircle.selection_collision line 130
  24. abbrev OAI.FiniteCircle.PartitionSpace line 149
  25. theorem OAI.FiniteCircle.finite_partition line 151
  26. theorem OAI.FiniteCircle.partition_separation_le line 182