Double counting

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.

• bipartiteBelow: s.bipartiteBelow r b are the elements of s below b w.r.t. 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 w.r.t. 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.

Implementation notes

For the formulation of double-counting arguments where a bipartite graph is considered as a bipartite simple graph G : SimpleGraph V, see Mathlib/Combinatorics/SimpleGraph/Bipartite.lean.

Bipartite graph

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

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

Equations

• Finset.bipartiteBelow r s b = {a ∈ s | r a b}

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

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

Equations

• Finset.bipartiteAbove r t a = {b ∈ t | r a b}

theorem Finset.bipartiteBelow_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [DecidablePred (r a)] : bipartiteBelow (Function.swap r) t a = bipartiteAbove r t a

theorem Finset.bipartiteAbove_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] : bipartiteAbove (Function.swap r) s b = bipartiteBelow r s b

@[simp]

theorem Finset.coe_bipartiteBelow {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] : ↑(bipartiteBelow r s b) = {a : α | a ∈ s ∧ r a b}

@[simp]

theorem Finset.coe_bipartiteAbove {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [DecidablePred (r a)] : ↑(bipartiteAbove r t a) = {b : β | b ∈ t ∧ r a b}

@[simp]

theorem Finset.mem_bipartiteBelow {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {b : β} [(a : α) → Decidable (r a b)] {a : α} : a ∈ bipartiteBelow r s b ↔ a ∈ s ∧ r a b

@[simp]

theorem Finset.mem_bipartiteAbove {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {t : Finset β} {a : α} [DecidablePred (r a)] {b : β} : b ∈ bipartiteAbove r t a ↔ b ∈ t ∧ r a b

theorem Finset.prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [CommMonoid R] (f : α → β → R) [(a : α) → (b : β) → Decidable (r a b)] : ∏ a ∈ s, ∏ b ∈ bipartiteAbove r t a, f a b = ∏ b ∈ t, ∏ a ∈ bipartiteBelow r s b, f a b

theorem Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [AddCommMonoid R] (f : α → β → R) [(a : α) → (b : β) → Decidable (r a b)] : ∑ a ∈ s, ∑ b ∈ bipartiteAbove r t a, f a b = ∑ b ∈ t, ∑ a ∈ bipartiteBelow r s b, f a b

theorem Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [(a : α) → (b : β) → Decidable (r a b)] : ∑ a ∈ s, (bipartiteAbove r t a).card = ∑ b ∈ t, (bipartiteBelow r s b).card

theorem Finset.card_nsmul_le_card_nsmul {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [Semiring R] [PartialOrder R] [IsOrderedRing R] {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (hm : ∀ a ∈ s, m ≤ ↑(bipartiteAbove r t a).card) (hn : ∀ b ∈ t, ↑(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_nsmul_le_card_nsmul' {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [Semiring R] [PartialOrder R] [IsOrderedRing R] {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (hn : ∀ b ∈ t, n ≤ ↑(bipartiteBelow r s b).card) (hm : ∀ a ∈ s, ↑(bipartiteAbove r t a).card ≤ m) : t.card • n ≤ s.card • m

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_nsmul_lt_card_nsmul_of_lt_of_le {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (hs : s.Nonempty) (hm : ∀ a ∈ s, m < ↑(bipartiteAbove r t a).card) (hn : ∀ b ∈ t, ↑(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 strict lower bound on the number of edges while the RHS is an upper bound.

theorem Finset.card_nsmul_lt_card_nsmul_of_le_of_lt {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (ht : t.Nonempty) (hm : ∀ a ∈ s, m ≤ ↑(bipartiteAbove r t a).card) (hn : ∀ b ∈ t, ↑(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 a strict upper bound.

theorem Finset.card_nsmul_lt_card_nsmul_of_lt_of_le' {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (ht : t.Nonempty) (hn : ∀ b ∈ t, n < ↑(bipartiteBelow r s b).card) (hm : ∀ a ∈ s, ↑(bipartiteAbove r t a).card ≤ m) : t.card • n < s.card • m

Double counting argument.

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

theorem Finset.card_nsmul_lt_card_nsmul_of_le_of_lt' {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [(a : α) → (b : β) → Decidable (r a b)] (hs : s.Nonempty) (hn : ∀ b ∈ t, n ≤ ↑(bipartiteBelow r s b).card) (hm : ∀ a ∈ s, ↑(bipartiteAbove r t a).card < m) : t.card • n < s.card • m

Double counting argument.

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

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

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

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

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

theorem Finset.sum_card_eq_sum_biUnion_card {α : Type u_2} {β : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq β] (B : α → Finset β) (s : Finset α) : ∑ j ∈ s, (B j).card = ∑ x ∈ s.biUnion B, {j : α | j ∈ s ∧ x ∈ B j}.card

Given a finite collection of finite subsets $B_1, \ldots, B_k$ and, for every $x \in \bigcup_i B_i$, let $C_x$ be the set of indices of the $B_i$'s that contain $x$. Then, $\sum_i |B_i| = \sum_x |C_x|$.

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

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