The convex hull of the permutation orbit of a vector

For a vector w : ι → R, its permutation orbit is the set of rearrangements w ∘ σ of its coordinates, and the convex hull of this orbit is the permutohedron of w. This file records two facts about this convex hull.

By Birkhoff's theorem every doubly stochastic matrix is a convex combination of permutation matrices, so the image M *ᵥ w of w under a doubly stochastic matrix M lies in the convex hull of the permutation orbit of w. This is how the diagonal of a symmetric operator in an orthonormal basis enters the permutohedron of its spectrum.

If the coordinates of w : ι → ℝ are pairwise at distance at least γ ≥ 0, then every point c of the convex hull of its permutation orbit satisfies the displacement estimate

(γ / √2) ‖w - c‖ ≤ ⟪w - c, w⟫,

with the Euclidean norm and inner product written as sums. For a single rearrangement c = w ∘ σ the right-hand side is ‖w - w ∘ σ‖² / 2, and a nontrivial rearrangement moves at least two coordinates, each by at least γ, so ‖w - w ∘ σ‖ ≥ √2 γ. The left side of the estimate is convex in c and the right side is affine, so the points where it holds form a convex set, and the estimate passes to the convex hull. The estimate is the convexity input to Davis's lower bound on the change of the eigenvalues of a symmetric operator.

For real w listed in decreasing order, Rado's theorem identifies the convex hull with the tuples majorized by w: those whose decreasing rearrangement has prefix sums at most those of w and whose total sum is that of w. One direction is the rearrangement inequality. For the other, the convex hull is closed under Robin Hood transfers, each being a convex combination of a point and its image under a transposition, so the transfer closure theorem applies.

Main results

• Matrix.mulVec_mem_convexHull_range_comp_perm: if M is doubly stochastic, then M *ᵥ w lies in the convex hull of the permutation orbit of w.
• Equiv.Perm.comp_perm_mem_convexHull_range_comp_perm_iff: the convex hull of a permutation orbit is permutation invariant.
• TauCeti.mul_sqrt_sum_sq_sub_le_sum_sub_mul_of_mem_convexHull: the separated-coordinate displacement estimate (γ / √2) ‖w - c‖ ≤ ⟪w - c, w⟫.
• TauCeti.mem_convexHull_range_comp_perm_iff, TauCeti.mem_convexHull_range_comp_perm_iff_of_antitone: Rado's theorem, the convex hull of the permutation orbit of a decreasing w consists of the tuples majorized by w.

References

• C. Davis, The rotation of eigenvectors by a perturbation, J. Math. Anal. Appl. 6 (1963), 159–173; the displacement estimate serves the eigenvalue-change bound of Theorem 4.1.
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer (2011), Chapter 2 (doubly stochastic matrices and Birkhoff's theorem).
• R. Rado, An inequality, J. London Math. Soc. 27 (1952), 1–6.

theorem Matrix.mulVec_mem_convexHull_range_comp_perm {R : Type u_1} {ι : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype ι] [DecidableEq ι] {M : Matrix ι ι R} (hM : M ∈ doublyStochastic R ι) (w : ι → R) : M.mulVec w ∈ (convexHull R) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)

Doubly stochastic images lie in the permutohedron. If M is doubly stochastic, then M *ᵥ w lies in the convex hull of the rearrangements w ∘ σ of w.

@[simp]

theorem Equiv.Perm.comp_perm_mem_convexHull_range_comp_perm_iff {R : Type u_1} {ι : Type u_2} [Semiring R] [PartialOrder R] {w x : ι → R} (τ : Perm ι) : x ∘ ⇑τ ∈ (convexHull R) (Set.range fun (σ : Perm ι) => w ∘ ⇑σ) ↔ x ∈ (convexHull R) (Set.range fun (σ : Perm ι) => w ∘ ⇑σ)

The convex hull of the permutation orbit of w is invariant under permutations of the coordinates: x ∘ τ lies in it exactly when x does.

theorem TauCeti.mul_sqrt_sum_sq_sub_le_sum_sub_mul_of_mem_convexHull {ι : Type u_1} [Fintype ι] {w c : ι → ℝ} {γ : ℝ} (hγ : 0 ≤ γ) (hw : Pairwise fun (i j : ι) => γ ≤ |w i - w j|) (hc : c ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)) : γ / √2 * √(∑ i : ι, (w i - c i) ^ 2) ≤ ∑ i : ι, (w i - c i) * w i

Separated-coordinate displacement estimate. Let γ ≥ 0 and let the coordinates of w : ι → ℝ be pairwise at distance at least γ. If c lies in the convex hull of the rearrangements w ∘ σ of w, then (γ / √2) ‖w - c‖ ≤ ⟪w - c, w⟫ for the Euclidean norm and inner product.

Majorization

theorem TauCeti.sum_eq_of_mem_convexHull_range_comp_perm {ι : Type u_1} [Fintype ι] {R : Type u_2} [Semiring R] [PartialOrder R] {w x : ι → R} (hx : x ∈ (convexHull R) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)) : ∑ i : ι, x i = ∑ i : ι, w i

Every point of the convex hull of the permutation orbit of w has the total sum of w.

theorem TauCeti.prefixSum_le_of_mem_convexHull_range_comp_perm {R : Type u_2} {n : ℕ} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {w x : Fin n → R} (hw : Antitone w) (hx : x ∈ (convexHull R) (Set.range fun (σ : Equiv.Perm (Fin n)) => w ∘ ⇑σ)) (k : ℕ) : prefixSum k x ≤ prefixSum k w

For antitone w, every point of the convex hull of the permutation orbit of w has prefix sums bounded by those of w.

theorem TauCeti.mem_convexHull_range_comp_perm_iff_of_antitone {n : ℕ} {w x : Fin n → ℝ} (hw : Antitone w) (hx : Antitone x) : x ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm (Fin n)) => w ∘ ⇑σ) ↔ (∀ (k : ℕ), prefixSum k x ≤ prefixSum k w) ∧ ∑ i : Fin n, x i = ∑ i : Fin n, w i

Rado's theorem for antitone tuples. For antitone w and x, the tuple x lies in the convex hull of the permutation orbit of w exactly when x is majorized by w: every prefix sum of x is at most the corresponding prefix sum of w, and the total sums agree.

theorem TauCeti.mem_convexHull_range_comp_perm_iff {n : ℕ} {w x : Fin n → ℝ} (hw : Antitone w) : x ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm (Fin n)) => w ∘ ⇑σ) ↔ (∀ (k : ℕ), prefixSum k (x ∘ ⇑(Tuple.sortDesc x)) ≤ prefixSum k w) ∧ ∑ i : Fin n, x i = ∑ i : Fin n, w i

Rado's theorem. For antitone w, a tuple x lies in the convex hull of the permutation orbit of w exactly when x is majorized by w: the prefix sums of the decreasing rearrangement of x are at most those of w, and the total sums agree.