Existence of staircase couplings

Two nonnegative finitely supported functions on linear orders with equal total mass admit nonnegative joint weights supported on a chain in the coordinatewise product order. This is the barycentric existence argument for the staircase triangulation of a product of simplices. The index orders are arbitrary, and the coefficients may lie in an ordered additive group or a monoid with truncated subtraction, such as ℕ or ℝ≥0. Normalization to mass one is unnecessary.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (triangulating products of polyhedra).

theorem Finsupp.exists_nonneg_isChain_mapDomain {α : Type u_1} {β : Type u_2} {R : Type u_3} [LinearOrder α] [LinearOrder β] [AddCommMonoid R] [LinearOrder R] [IsOrderedCancelAddMonoid R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (f : α →₀ R) (g : β →₀ R) (hf : 0 ≤ f) (hg : 0 ≤ g) (hmass : (f.sum fun (x : α) (r : R) => r) = g.sum fun (x : β) (r : R) => r) : ∃ (w : α × β →₀ R), 0 ≤ w ∧ IsChain (fun (x1 x2 : α × β) => x1 ≤ x2) ↑w.support ∧ mapDomain Prod.fst w = f ∧ mapDomain Prod.snd w = g

Nonnegative finite weights of equal total mass have a nonnegative coupling supported on a staircase. The two mapDomain equations specify its marginals.