Documentation

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

bipartiteBelow: s.bipartiteBelow r b are the elements of s below b wrt to r. Its size is the number of edges of b in s.
bipartiteAbove: 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.bipartiteBelow {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (s : Finset α) (b : β) [inst : (a : α) → Decidable (r a b)] :

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

Equations

Finset.bipartiteBelow r s b = Finset.filter (fun a => r a b) s

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

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

Equations

Finset.bipartiteAbove r t a = Finset.filter (r a) t

theorem Finset.bipartiteBelow_swap {α : Type u_2} {β : Type u_1} (r : α → β → Prop) (t : Finset β) (a : α) [inst : DecidablePred (r a)] :

Finset.bipartiteBelow (Function.swap r) t a = Finset.bipartiteAbove r t a

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

Finset.bipartiteAbove (Function.swap r) s b = Finset.bipartiteBelow r s b

@[simp]

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

↑(Finset.bipartiteBelow r s b) = { a | a ∈ s ∧ r a b }

@[simp]

theorem Finset.coe_bipartiteAbove {α : Type u_2} {β : Type u_1} (r : α → β → Prop) (t : Finset β) (a : α) [inst : 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 : β} [inst : (a : α) → Decidable (r a b)] {a : α} :

a ∈ Finset.bipartiteBelow r s b ↔ a ∈ s ∧ r a b

@[simp]

theorem Finset.mem_bipartiteAbove {α : Type u_2} {β : Type u_1} (r : α → β → Prop) {t : Finset β} {a : α} [inst : 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 β} [inst : (a : α) → (b : β) → Decidable (r a b)] :

(Finset.sum s fun a => Finset.card (Finset.bipartiteAbove r t a)) = Finset.sum t fun b => Finset.card (Finset.bipartiteBelow r s b)

theorem Finset.card_mul_le_card_mul {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m : ℕ} {n : ℕ} [inst : (a : α) → (b : β) → Decidable (r a b)] (hm : ∀ (a : α), a ∈ s → m ≤ Finset.card (Finset.bipartiteAbove r t a)) (hn : ∀ (b : β), b ∈ t → Finset.card (Finset.bipartiteBelow r s b) ≤ n) :

Finset.card s * m ≤ Finset.card t * 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_2} {β : Type u_1} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m : ℕ} {n : ℕ} [inst : (a : α) → (b : β) → Decidable (r a b)] (hn : ∀ (b : β), b ∈ t → n ≤ Finset.card (Finset.bipartiteBelow r s b)) (hm : ∀ (a : α), a ∈ s → Finset.card (Finset.bipartiteAbove r t a) ≤ m) :

Finset.card t * n ≤ Finset.card s * m

theorem Finset.card_mul_eq_card_mul {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m : ℕ} {n : ℕ} [inst : (a : α) → (b : β) → Decidable (r a b)] (hm : ∀ (a : α), a ∈ s → Finset.card (Finset.bipartiteAbove r t a) = m) (hn : ∀ (b : β), b ∈ t → Finset.card (Finset.bipartiteBelow r s b) = n) :

Finset.card s * m = Finset.card t * 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 → Set.Subsingleton { a | a ∈ s ∧ r a b }) :

Finset.card s ≤ Finset.card t

theorem Finset.card_le_card_of_forall_subsingleton' {α : Type u_2} {β : Type u_1} (r : α → β → Prop) {s : Finset α} {t : Finset β} (ht : ∀ (b : β), b ∈ t → ∃ a, a ∈ s ∧ r a b) (hs : ∀ (a : α), a ∈ s → Set.Subsingleton { b | b ∈ t ∧ r a b }) :

Finset.card t ≤ Finset.card s

theorem Fintype.card_le_card_of_leftTotal_unique {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] {r : α → β → Prop} (h₁ : Relator.LeftTotal r) (h₂ : Relator.LeftUnique r) :

Fintype.card α ≤ Fintype.card β

theorem Fintype.card_le_card_of_rightTotal_unique {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] {r : α → β → Prop} (h₁ : Relator.RightTotal r) (h₂ : Relator.RightUnique r) :

Fintype.card β ≤ Fintype.card α