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
.
bipartiteBelow
:s.bipartiteBelow r b
are the elements ofs
belowb
wrt tor
. Its size is the number of edges ofb
ins
.bipartiteAbove
:t.bipartite_Above r a
are the elements oft
abovea
wrt tor
. Its size is the number of edges ofa
int
.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.bipartiteAbove
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(t : Finset β)
(a : α)
[DecidablePred (r a)]
:
Finset β
Elements of t
which are "above" a
according to relation r
.
Instances For
theorem
Finset.bipartiteBelow_swap
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(t : Finset β)
(a : α)
[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 : β)
[(a : α) → Decidable (r a b)]
:
Finset.bipartiteAbove (Function.swap r) s b = Finset.bipartiteBelow r s 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_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.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 : ℕ}
[(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_1}
{β : Type u_2}
(r : α → β → Prop)
{s : Finset α}
{t : Finset β}
{m : ℕ}
{n : ℕ}
[(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 : ℕ}
[(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_1}
{β : Type u_2}
(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}
[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)
: