Documentation

Mathlib.Combinatorics.Enumerative.DoubleCounting

Double countings #

This file gathers a few double counting arguments.

Bipartite graphs #

In a bipartite graph (considered as a relation r : α → β → Prop), we can bound the number of edges between s : Finset α and t : Finset β by the minimum/maximum of edges over all a ∈ s times the size of s. Similarly for t. Combining those two yields inequalities between the sizes of s and t.

Bipartite graph #

def Finset.bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] :

Elements of s which are "below" b according to relation r.

Equations
Instances For
    def Finset.bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) (t : Finset β) (a : α) [DecidablePred (r a)] :

    Elements of t which are "above" a according to relation r.

    Equations
    Instances For
      theorem Finset.bipartiteBelow_swap {α : Type u_1} {β : Type u_2} (r : αβProp) (t : Finset β) (a : α) [DecidablePred (r a)] :
      theorem Finset.bipartiteAbove_swap {α : Type u_1} {β : Type u_2} (r : αβProp) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] :
      @[simp]
      theorem Finset.coe_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] :
      (Finset.bipartiteBelow r s b) = {a : α | a s r a b}
      @[simp]
      theorem Finset.coe_bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) (t : Finset β) (a : α) [DecidablePred (r a)] :
      (Finset.bipartiteAbove r t a) = {b : β | b t r a b}
      @[simp]
      theorem Finset.mem_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {b : β} [(a : α) → Decidable (r a b)] {a : α} :
      a Finset.bipartiteBelow r s b a s r a b
      @[simp]
      theorem Finset.mem_bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) {t : Finset β} {a : α} [DecidablePred (r a)] {b : β} :
      b Finset.bipartiteAbove r t a b t r a b
      theorem Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} [(a : α) → (b : β) → Decidable (r a b)] :
      (Finset.sum s fun (a : α) => (Finset.bipartiteAbove r t a).card) = Finset.sum t fun (b : β) => (Finset.bipartiteBelow r s b).card
      theorem Finset.card_mul_le_card_mul {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hm : as, m (Finset.bipartiteAbove r t a).card) (hn : bt, (Finset.bipartiteBelow r s b).card n) :
      s.card * m t.card * n

      Double counting argument. Considering r as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS is an upper bound.

      theorem Finset.card_mul_le_card_mul' {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hn : bt, n (Finset.bipartiteBelow r s b).card) (hm : as, (Finset.bipartiteAbove r t a).card m) :
      t.card * n s.card * m
      theorem Finset.card_mul_eq_card_mul {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hm : as, (Finset.bipartiteAbove r t a).card = m) (hn : bt, (Finset.bipartiteBelow r s b).card = n) :
      s.card * m = t.card * n
      theorem Finset.card_le_card_of_forall_subsingleton {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} (hs : as, ∃ b ∈ t, r a b) (ht : bt, Set.Subsingleton {a : α | a s r a b}) :
      s.card t.card
      theorem Finset.card_le_card_of_forall_subsingleton' {α : Type u_1} {β : Type u_2} (r : αβProp) {s : Finset α} {t : Finset β} (ht : bt, ∃ a ∈ s, r a b) (hs : as, Set.Subsingleton {b : β | b t r a b}) :
      t.card s.card
      theorem Fintype.card_le_card_of_leftTotal_unique {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {r : αβProp} (h₁ : Relator.LeftTotal r) (h₂ : Relator.LeftUnique r) :
      theorem Fintype.card_le_card_of_rightTotal_unique {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {r : αβProp} (h₁ : Relator.RightTotal r) (h₂ : Relator.RightUnique r) :