mathlib3 documentation

combinatorics.double_counting

Double countings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 the size of s. Similarly for t. Combining those two yields inequalities between the sizes of s and t.

bipartite_below: s.bipartite_below r b are the elements of s below b wrt to r. Its size is the number of edges of b in s.
bipartite_above: t.bipartite_above r a are the elements of t above a wrt to r. Its size is the number of edges of a in t.
card_mul_le_card_mul, card_mul_le_card_mul': Double counting the edges of a bipartite graph from below and from above.
card_mul_eq_card_mul: Equality combination of the previous.

Bipartite graph #

def finset.bipartite_below {α : 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

finset.bipartite_below r s b = finset.filter (λ (a : α), r a b) s

def finset.bipartite_above {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (t : finset β) (a : α) [decidable_pred (r a)] :

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

Equations

finset.bipartite_above r t a = finset.filter (r a) t

theorem finset.bipartite_below_swap {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (t : finset β) (a : α) [decidable_pred (r a)] :

finset.bipartite_below (function.swap r) t a = finset.bipartite_above r t a

theorem finset.bipartite_above_swap {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (s : finset α) (b : β) [Π (a : α), decidable (r a b)] :

finset.bipartite_above (function.swap r) s b = finset.bipartite_below r s b

@[simp, norm_cast]

theorem finset.coe_bipartite_below {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (s : finset α) (b : β) [Π (a : α), decidable (r a b)] :

↑(finset.bipartite_below r s b) = {a ∈ ↑s | r a b}

@[simp, norm_cast]

theorem finset.coe_bipartite_above {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (t : finset β) (a : α) [decidable_pred (r a)] :

↑(finset.bipartite_above r t a) = {b ∈ ↑t | r a b}

@[simp]

theorem finset.mem_bipartite_below {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {s : finset α} {b : β} [Π (a : α), decidable (r a b)] {a : α} :

a ∈ finset.bipartite_below r s b ↔ a ∈ s ∧ r a b

@[simp]

theorem finset.mem_bipartite_above {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {t : finset β} {a : α} [decidable_pred (r a)] {b : β} :

b ∈ finset.bipartite_above r t a ↔ b ∈ t ∧ r a b

theorem finset.sum_card_bipartite_above_eq_sum_card_bipartite_below {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {s : finset α} {t : finset β} [Π (a : α) (b : β), decidable (r a b)] :

s.sum (λ (a : α), (finset.bipartite_above r t a).card) = t.sum (λ (b : β), (finset.bipartite_below 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 : ∀ (a : α), a ∈ s → m ≤ (finset.bipartite_above r t a).card) (hn : ∀ (b : β), b ∈ t → (finset.bipartite_below 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 : ∀ (b : β), b ∈ t → n ≤ (finset.bipartite_below r s b).card) (hm : ∀ (a : α), a ∈ s → (finset.bipartite_above 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 : ∀ (a : α), a ∈ s → (finset.bipartite_above r t a).card = m) (hn : ∀ (b : β), b ∈ t → (finset.bipartite_below 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 : ∀ (a : α), a ∈ s → (∃ (b : β), b ∈ t ∧ r a b)) (ht : ∀ (b : β), b ∈ t → {a ∈ ↑s | r a b}.subsingleton) :

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 : ∀ (b : β), b ∈ t → (∃ (a : α), a ∈ s ∧ r a b)) (hs : ∀ (a : α), a ∈ s → {b ∈ ↑t | r a b}.subsingleton) :

t.card ≤ s.card

theorem fintype.card_le_card_of_left_total_unique {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {r : α → β → Prop} (h₁ : relator.left_total r) (h₂ : relator.left_unique r) :

fintype.card α ≤ fintype.card β

theorem fintype.card_le_card_of_right_total_unique {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {r : α → β → Prop} (h₁ : relator.right_total r) (h₂ : relator.right_unique r) :

fintype.card β ≤ fintype.card α