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.
bipartite_below:s.bipartite_below r bare the elements ofsbelowbwrt tor. Its size is the number of edges ofbins.bipartite_above:t.bipartite_above r aare the elements oftaboveawrt tor. Its size is the number of edges ofaint.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)] :
finset α
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)] :
finset β
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]
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) :
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) :
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) :