OAI/Combinatorics/BalancedRyser/Probability/PatternLabelRestriction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.PatternModel.restrictLabels line 14
  2. theorem OAI.Balanced.PatternModel.restrictLabels_measure line 26
  3. theorem OAI.Balanced.PatternModel.restrictLabels_fixCoordinates line 29
  4. theorem OAI.Balanced.PatternModel.restrictLabels_fixedExpectation line 33
  5. theorem OAI.Balanced.PatternModel.restrictLabels_indicator line 37
  6. theorem OAI.Balanced.PatternModel.restrictLabels_support line 41
  7. theorem OAI.Balanced.PatternModel.restrictLabels_count line 45
  8. theorem OAI.Balanced.PatternModel.restrictLabels_count_fun line 51
  9. theorem OAI.Balanced.PatternModel.restrictLabels_overlapCount line 55
  10. theorem OAI.Balanced.PatternModel.restrictLabels_support_card_le line 65
  11. theorem OAI.Balanced.PatternModel.restrictLabels_count_mem_Icc line 69
  12. theorem OAI.Balanced.PatternModel.restrictLabels_count_le line 76
  13. theorem OAI.Balanced.PatternTails.restricted_family_raw_tail line 89
  14. theorem OAI.Balanced.PatternTails.restricted_family_centered_tail line 113