Sums over finite types

A sum of values that are all equal to d on the indices satisfying p, and zero elsewhere, is the number of such indices times d (Fintype.sum_ite_eq_card_nsmul).

For a finite type ι and finite coordinate sets s i, a sum over maps taking their ith value in s i of a quantity depending only on two distinct coordinates is a sum over the pairs of values, with each pair counted once for every choice of the remaining coordinates. Counting arguments use this to reduce a sum over labelled copies of a pattern to a sum over one pair of its vertices.

More generally, any sum over such a box splits at two distinct coordinates i and j: sum over the maps with prescribed values at i and j, and then over all values of the two coordinates, substituted with Function.update. Telescoping arguments use this to test one pair of coordinates while the others stay fixed. The same splitting at three distinct coordinates tests one triple of coordinates.

Splitting at a single coordinate e averages it out: if G does not see the value at e, the sum of a (f e) * G f over all maps f vanishes as soon as a sums to zero (Fintype.sum_apply_mul_eq_zero). Second-moment computations over uniformly random colorings use this to discard every term containing a coordinate that occurs only once.

theorem Fintype.sum_ite_eq_card_nsmul {ι : Type u_1} {M : Type u_2} [Fintype ι] [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] {f : ι → M} {d : M} (hf : ∀ (i : ι), p i → f i = d) : (∑ i : ι, if p i then f i else 0) = card { i : ι // p i } • d

A sum of values f i over the indices satisfying p, all of which are equal to d, is the number of such indices times d.

theorem Fintype.sum_piFinset_apply_apply {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] {i j : ι} (hij : i ≠ j) (s : ι → Finset κ) (F : κ → κ → M) : ∑ g ∈ piFinset s, F (g i) (g j) = (∏ k ∈ Finset.univ \ {i, j}, (s k).card) • ∑ x ∈ s i, ∑ y ∈ s j, F x y

A sum of a function of two distinct coordinates over a finite box counts each pair of values once for every choice of the remaining coordinates.

theorem Fintype.sum_piFinset_eq_sum_filter_sum_sum_update {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [DecidableEq κ] [AddCommMonoid M] {i j : ι} (hij : i ≠ j) (s : ι → Finset κ) {a b : κ} (ha : a ∈ s i) (hb : b ∈ s j) (F : (ι → κ) → M) : ∑ g ∈ piFinset s, F g = ∑ h ∈ piFinset s with h i = a ∧ h j = b, ∑ x ∈ s i, ∑ y ∈ s j, F (Function.update (Function.update h i x) j y)

A sum over a finite box splits at two distinct coordinates i and j: for values a ∈ s i and b ∈ s j, each map in the box arises exactly once by overwriting the ith and jth values of a map in the box taking the values a at i and b at j.

theorem Fintype.sum_piFinset_eq_sum_filter_sum_sum_sum_update {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [DecidableEq κ] [AddCommMonoid M] {i j l : ι} (hij : i ≠ j) (hil : i ≠ l) (hjl : j ≠ l) (s : ι → Finset κ) {a b c : κ} (ha : a ∈ s i) (hb : b ∈ s j) (hc : c ∈ s l) (F : (ι → κ) → M) : ∑ g ∈ piFinset s, F g = ∑ h ∈ piFinset s with h i = a ∧ h j = b ∧ h l = c, ∑ x ∈ s i, ∑ y ∈ s j, ∑ z ∈ s l, F (Function.update (Function.update (Function.update h i x) j y) l z)

A sum over a finite box splits at three distinct coordinates i, j and l: for values a ∈ s i, b ∈ s j and c ∈ s l, each map in the box arises exactly once by overwriting the ith, jth and lth values of a map in the box taking the values a, b and c there.

theorem Fintype.sum_apply_mul_eq_zero {ι : Type u_1} {α : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [NonUnitalNonAssocSemiring R] (e : ι) {a : α → R} (ha : ∑ v : α, a v = 0) {G : (ι → α) → R} (hG : ∀ (f : ι → α) (v : α), G (Function.update f e v) = G f) : ∑ f : ι → α, a (f e) * G f = 0

Averaging out one coordinate. If a sums to zero and G does not depend on the value of its argument at e, then summing a (f e) * G f over all maps f : ι → α gives zero.