Comparing two sums when one index set dominates the other

Two finite sets of the same size, one of which carries a strictly larger weight at every point than the other, have strictly ordered sums (TauCeti.sum_lt_sum_of_forall_lt): the sizes agreeing is what makes the comparison work without any pointwise pairing of the two sets, since any bijection between them compares the weights termwise.

TauCeti.sum_lt_sum_image_sdiff is the form in which the comparison is used. A permutation σ of a finite set X that does not map a part A of it to itself must move some point of A out of A; if A carries the larger weights, the image of the complementary part X \ A therefore weighs strictly more than X \ A itself. The two sums involved differ only on the points that σ moves in or out of X \ A, and those are compared by the previous lemma.

The weights take values in an additive commutative monoid preordered so that addition is strictly monotone, which is what compares two sums of the same length termwise, and what turns the comparison of the parts on which the two sums differ into a comparison of the sums themselves.

theorem TauCeti.sum_lt_sum_of_forall_lt {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] (f : α → M) {U V : Finset α} (hcard : V.card = U.card) (hU : U.Nonempty) (hlt : ∀ u ∈ U, ∀ v ∈ V, f v < f u) : ∑ v ∈ V, f v < ∑ u ∈ U, f u

A set whose weights are all smaller than those of a second set of the same size has the smaller sum. The two sets have the same size, so some bijection matches them up, and along it every weight of the first set is smaller than the weight of its partner.

theorem TauCeti.sum_lt_sum_image_sdiff {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] [DecidableEq α] (f : α → M) {X A : Finset α} {σ : Equiv.Perm α} (hAX : A ⊆ X) (hXimg : Finset.image (⇑σ) X = X) (himg : Finset.image (⇑σ) A ≠ A) (hlt : ∀ a ∈ A, ∀ b ∈ X \ A, f b < f a) : ∑ z ∈ X \ A, f z < ∑ z ∈ Finset.image (⇑σ) (X \ A), f z

A permutation of a set that does not preserve a prescribed part increases the sum over the other part. If every weight of A exceeds every weight of X \ A, and σ permutes X without mapping A to itself, then σ moves some point of A into the image of X \ A, exchanging a point for one of strictly larger weight, so that image has the larger sum.