OAI/Combinatorics/BalancedRyser/Probability/PatternMoments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.PatternMoments.expectation line 11
  2. lemma OAI.Balanced.PatternMoments.expectation_sum line 13
  3. lemma OAI.Balanced.PatternMoments.expectation_mul_const line 19
  4. lemma OAI.Balanced.PatternMoments.expectation_const_mul line 23
  5. theorem OAI.Balanced.PatternMoments.weighted_fiber_bound line 27
  6. def OAI.Balanced.PatternMoments.count line 61
  7. lemma OAI.Balanced.PatternMoments.power_expansion line 63
  8. theorem OAI.Balanced.PatternMoments.moment_bound_of_prefix_bounds line 70
  9. def OAI.Balanced.PatternMoments.scheduledWeight line 102
  10. def OAI.Balanced.PatternMoments.scheduleCost line 110
  11. lemma OAI.Balanced.PatternMoments.scheduleCost_nonneg line 114
  12. theorem OAI.Balanced.PatternMoments.scheduledWeight_le line 122
  13. def OAI.Balanced.PatternMoments.rootCount line 166
  14. lemma OAI.Balanced.PatternMoments.scheduleCost_eq line 170
  15. theorem OAI.Balanced.PatternMoments.scheduleCost_le_power line 177
  16. def OAI.Balanced.PatternMoments.scheduleAllowed line 185
  17. theorem OAI.Balanced.PatternMoments.scheduledWeight_eq_sum line 192
  18. theorem OAI.Balanced.PatternMoments.scheduledWeight_eq_sum_of_length line 217
  19. theorem OAI.Balanced.PatternMoments.sum_le_card_mul_of_reordered_cover line 227
  20. def OAI.Balanced.PatternMoments.tuplePermutation line 262
  21. theorem OAI.Balanced.PatternMoments.weighted_ordering_bound line 268