The bag-counting identity of a clique tree

For every clique tree, the bag sizes and the sizes of the separators sitting on the tree edges recover the number of vertices: ∑ i, |bag i| − ∑ (tree edges i → j), |bag i ∩ bag j| = |V|. This is the general form of the perfect-elimination-order count SimpleGraph.IsPEO.card_edgeFinset_add_card_eq_sum_card_peoBag, and the companion of the edge count SimpleGraph.CliqueTree.card_edgeFinset_eq_sum_fiber.

The proof is a double count: a vertex v lies in the bags of a nonempty set of nodes, exactly one of which — the node top v — does not pass v on to its parent.

Main definitions

• SimpleGraph.CliqueTree.parentSep — the separator attached to a node: bag i ∩ bag (parent i), and ∅ at a root.

Main results

• SimpleGraph.CliqueTree.card_eq_sum_card_bag_sub_sum_card_inter

def SimpleGraph.CliqueTree.parentSep {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [DecidableEq V] (T : G.CliqueTree ι) (i : ι) : Finset V

The separator of the tree edge above i: the intersection of bag i with the bag of its parent, and ∅ if i is a root.

Equations

• T.parentSep i = (T.parent i).elim ∅ fun (j : ι) => T.bag i ∩ T.bag j

theorem SimpleGraph.CliqueTree.parentSep_eq_of_parent {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [DecidableEq V] {T : G.CliqueTree ι} {i j : ι} (h : T.parent i = some j) : T.parentSep i = T.bag i ∩ T.bag j

theorem SimpleGraph.CliqueTree.parentSep_eq_empty_of_root {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [DecidableEq V] {T : G.CliqueTree ι} {i : ι} (h : T.parent i = none) : T.parentSep i = ∅

theorem SimpleGraph.CliqueTree.card_parentSep {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [DecidableEq V] (T : G.CliqueTree ι) (i : ι) : (T.parentSep i).card = (T.parent i).elim 0 fun (j : ι) => (T.bag i ∩ T.bag j).card

theorem SimpleGraph.CliqueTree.mem_parentSep_iff {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [DecidableEq V] {T : G.CliqueTree ι} {i : ι} {v : V} : v ∈ T.parentSep i ↔ v ∈ T.bag i ∧ i ≠ T.top v

The vertices of the separator above i are exactly the vertices of bag i that i passes on to its parent, i.e. the vertices of bag i whose top node is not i.

theorem SimpleGraph.CliqueTree.card_eq_sum_card_bag_sub_sum_card_inter {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] (T : G.CliqueTree ι) : (Fintype.card V + ∑ i : ι, (T.parent i).elim 0 fun (j : ι) => (T.bag i ∩ T.bag j).card) = ∑ i : ι, (T.bag i).card

The bag-counting identity. The total bag size, minus the total size of the separators sitting on the edges of the clique tree, is the number of vertices.

theorem SimpleGraph.CliqueTree.card_add_sum_card_parentSep {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] (T : G.CliqueTree ι) : Fintype.card V + ∑ i : ι with (T.parent i).isSome = true, (T.parentSep i).card = ∑ i : ι, (T.bag i).card

The bag-counting identity, summed over the edges of the tree. Only the non-root nodes, the ones carrying a tree edge, contribute a separator.