Bounded differences on a finite product

A function on a finite product ι → β, valued in a linearly ordered additive commutative group, has bounded differences with bounds c : ι → α when changing a single coordinate i, leaving the others fixed, moves the value by at most c i. TauCeti.abs_sub_le_of_bounded_differences telescopes that coordinatewise hypothesis into a global one: any two points of the product, however many coordinates they differ in, have values at most ∑ i, c i apart.

The argument changes the coordinates one at a time, using Function.update to interpolate between the two points, and adds up the resulting one-coordinate bounds with the triangle inequality. It is stated for an arbitrary finite index type and does not require the bounds to be nonnegative.

This is the combinatorial half of McDiarmid's bounded-differences inequality, proved in TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences; it involves no probability and is kept separate from it.

theorem TauCeti.abs_sub_le_of_bounded_differences {ι : Type u_1} [Fintype ι] {α : Type u_2} {β : Type u_3} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (c : ι → α) (f : (ι → β) → α) (hbd : ∀ (i : ι) (x x' : ι → β), (∀ (l : ι), l ≠ i → x l = x' l) → |f x - f x'| ≤ c i) (x x' : ι → β) : |f x - f x'| ≤ ∑ i : ι, c i

A function with bounded differences varies by at most the sum of its coordinate bounds. If changing coordinate i moves f by at most c i, then changing every coordinate moves it by at most ∑ i, c i.