Regrouping a finite sum by the fibres of a map

A sum over a finite type can be taken fibrewise along any map out of it: sum over the values the map actually takes, and within each value over the indices sent there.

Mathlib's Fintype.sum_fiberwise says this with the outer sum ranging over the whole codomain, which needs the codomain finite. The version here indexes the outer sum by the image instead, so it applies to a map into an arbitrary type — the situation whenever the codomain is a quotient or a subtype with no finiteness available.

Regrouping along the coordinate projections of a finite dependent product turns a sum whose summand is weighted by a sum of coordinate functions into a sum of one-coordinate sums against the fibrewise masses; this is the algebraic core of multi-marginal linear programming.

Fibres over values the map does not take are empty, so a bound below 0 that holds for the fibre sums over the range holds for the fibre sum over every value of the codomain.

Main results

• TauCeti.sum_eq_sum_image_fiber: ∑ i, F i is the sum, over the values g takes, of the sums of F over the fibres of g.
• TauCeti.sum_sum_eval_mul: summing (∑ i, φ i (z i)) * f z over a finite dependent product regroups, coordinate by coordinate, into ∑ i, ∑ a, φ i a * ∑ z with z i = a, f z.
• TauCeti.lt_sum_filter_eq_of_forall_apply: a negative lower bound for the fibre sums of g over its range is a lower bound for the fibre sum over every value.

theorem TauCeti.sum_eq_sum_image_fiber {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq κ] [AddCommMonoid M] (g : ι → κ) (F : ι → M) : ∑ i : ι, F i = ∑ k ∈ Finset.image g Finset.univ, ∑ i : { i : ι // g i = k }, F ↑i

A finite sum is the sum over the values actually taken of the sums over their fibres. Summing F over all of ι is summing, over each k in the image of g, the contribution of the indices g sends to k.

The outer index is Finset.univ.image g rather than all of κ, so no finiteness of κ is needed; that is the difference from Fintype.sum_fiberwise.

theorem TauCeti.sum_sum_eval_mul {ι : Type u_1} {X : ι → Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (X i)] [(i : ι) → DecidableEq (X i)] [NonUnitalNonAssocSemiring R] (φ : (i : ι) → X i → R) (f : ((i : ι) → X i) → R) : ∑ z : (i : ι) → X i, (∑ i : ι, φ i (z i)) * f z = ∑ i : ι, ∑ a : X i, φ i a * ∑ z : (i : ι) → X i with z i = a, f z

Regrouping a product-indexed sum by coordinates. Summing f against a weight that is a sum of one-coordinate functions is the same as summing, for each coordinate i and each value a there, the value φ i a against the mass f puts on the fibre {z | z i = a}.

theorem TauCeti.lt_sum_filter_eq_of_forall_apply {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq κ] [AddCommMonoid M] [LT M] {g : ι → κ} {F : ι → M} {c : M} (hc : c < 0) (h : ∀ (j : ι), c < ∑ i : ι with g i = g j, F i) (k : κ) : c < ∑ i : ι with g i = k, F i

A negative lower bound on the fibre sums over the range bounds every fibre sum. If c < 0 bounds from below the sum of F over each fibre of g above a value of g, then it bounds the sum of F over the fibre above any k.