OAI/Analysis/LipschitzFree/ColorCounting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Counting colorings subject to vertex constraints

  1. def OAI.DiscreteFree.ColorCounting.coloringEquiv line 17
  2. theorem OAI.DiscreteFree.ColorCounting.coloringEquiv_fst line 37
  3. def OAI.DiscreteFree.ColorCounting.goodColoringEquiv line 40
  4. theorem OAI.DiscreteFree.ColorCounting.cardinal_identity line 63
  5. theorem OAI.DiscreteFree.ColorCounting.cardinal_bound line 79
  6. theorem OAI.DiscreteFree.ColorCounting.union_bound line 97
  7. theorem OAI.DiscreteFree.ColorCounting.weighted_union_bound line 106
  8. theorem OAI.DiscreteFree.ColorCounting.many_walks_bound line 117
  9. theorem OAI.DiscreteFree.ColorCounting.colored_roots_bound line 133