Sums over intervals of graphs on a finite vertex set

On a finite vertex set, G ↦ G.edgeFinset maps the graphs between F and H bijectively onto the finsets of pairs between F.edgeFinset and H.edgeFinset. Consequently a sum over an interval of graphs, of a summand that depends on the graph only through its edge set, is a sum over an interval of the Boolean lattice Finset (Sym2 V), where the finset interval API applies.

Main results

• SimpleGraph.sum_filter_le_le_eq_sum_Icc_edgeFinset — a sum over the graphs between F and H of a function of their edge finsets is the sum of that function over Finset.Icc F.edgeFinset H.edgeFinset.

theorem SimpleGraph.sum_filter_le_le_eq_sum_Icc_edgeFinset {V : Type u_1} {M : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid M] (F H : SimpleGraph V) [DecidablePred fun (G : SimpleGraph V) => F ≤ G ∧ G ≤ H] [(G : SimpleGraph V) → Fintype ↑G.edgeSet] (f : Finset (Sym2 V) → M) : ∑ G : SimpleGraph V with F ≤ G ∧ G ≤ H, f G.edgeFinset = ∑ s ∈ Finset.Icc F.edgeFinset H.edgeFinset, f s

Summing a function of the edge finset over the graphs between F and H is summing it over the edge finsets between theirs.