Weak majorization and transfer descent

For real tuples x y : Fin n → ℝ, the prefix sum prefixSum k x is the sum of the first k coordinates of x. For antitone nonnegative tuples, x is weakly majorized by y (often written x ≺w y) when every prefix sum of x is at most the corresponding prefix sum of y.

A set of real tuples is symmetric convex when it is convex, invariant under permutations of the coordinates, and invariant under changing the sign of one coordinate. Such a set is solid (it contains every tuple dominated coordinatewise in absolute value by one of its members) and closed under Robin Hood transfers, which move mass from a larger coordinate to a smaller one. The main theorem is the transfer descent: a symmetric convex set containing y contains every antitone nonnegative z whose prefix sums are bounded by those of y. No ordering or sign condition is needed on y; in particular, it applies to every pair z ≺w y.

Without sign invariance, transfers alone reach every antitone tuple d with the total sum of y and prefix sums bounded by those of y (the transfer closure): for antitone y this is the statement that every tuple majorized by y arises from y by finitely many Robin Hood transfers. It applies to sets that are not known to be convex, such as the diagonals of a symmetric operator in all orthonormal bases.

Applied to the sublevel sets of a symmetric gauge (a seminorm invariant under permutations and sign changes of the coordinates), the descent shows that symmetric gauges are monotone for weak majorization. This is the convex engine behind Ky Fan dominance: once singular values are compared by their Ky Fan sums, every symmetric gauge of them is compared at once.

Main definitions

• TauCeti.IsWeaklyMajorizedBy x y: weak majorization of antitone nonnegative tuples.
• TauCeti.robinHood x i j δ: the transfer of δ from coordinate i to coordinate j.
• TauCeti.IsTTransform x y: y is a Robin Hood transfer of x followed by a permutation of the coordinates.
• TauCeti.IsSymmetricConvex K: K is convex, permutation invariant, and sign invariant.
• Seminorm.IsSymmetricGauge p: the seminorm p is a symmetric gauge; the sup norm is one, Seminorm.isSymmetricGauge_normSeminorm, and so is every ℓᵖ norm with 1 ≤ p, Seminorm.isSymmetricGauge_piLp.

Main results

• TauCeti.mem_of_prefixSum_le_of_sum_eq: transfer closure.
• Convex.robinHood_mem: a convex set containing a tuple and its swap contains the Robin Hood transfers between the swapped coordinates.
• TauCeti.IsSymmetricConvex.isSolid: symmetric convex sets are solid.
• TauCeti.IsSymmetricConvex.robinHood_mem: symmetric convex sets are closed under Robin Hood transfers.
• TauCeti.IsSymmetricConvex.mem_of_prefixSum_le: transfer descent.
• Seminorm.IsSymmetricGauge.apply_le_of_prefixSum_le, TauCeti.IsWeaklyMajorizedBy.apply_le: symmetric gauges are monotone for weak majorization.
• Seminorm.IsSymmetricGauge.apply_le_of_abs_le: symmetric gauges are monotone in the absolute values of the coordinates.
• Seminorm.IsSymmetricGauge.ext_of_antitone: symmetric gauges are determined by their values on nonincreasing nonnegative tuples.

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §II.1 and §IV.1.
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer (2011), §1.A and §2.B.
• G. H. Hardy, J. E. Littlewood, G. Pólya, Some simple inequalities satisfied by convex functions, Messenger Math. 58 (1929), 145–152, for the reduction of majorization to transfers.

Weak majorization

structure TauCeti.IsWeaklyMajorizedBy {n : ℕ} (x y : Fin n → ℝ) : Prop

The antitone nonnegative tuple x is weakly majorized by the antitone nonnegative tuple y (often written x ≺w y) when prefixSum k x ≤ prefixSum k y for every k.

• antitone_left : Antitone x
• antitone_right : Antitone y
• nonneg_left : 0 ≤ x
• nonneg_right : 0 ≤ y
• prefixSum_le (k : ℕ) : prefixSum k x ≤ prefixSum k y

theorem TauCeti.IsWeaklyMajorizedBy.refl {n : ℕ} {x : Fin n → ℝ} (hx : Antitone x) (hx0 : 0 ≤ x) : IsWeaklyMajorizedBy x x

Every antitone nonnegative tuple weakly majorizes itself.

theorem TauCeti.IsWeaklyMajorizedBy.trans {n : ℕ} {x y z : Fin n → ℝ} (hxy : IsWeaklyMajorizedBy x y) (hyz : IsWeaklyMajorizedBy y z) : IsWeaklyMajorizedBy x z

Weak majorization is transitive.

theorem TauCeti.IsWeaklyMajorizedBy.add {n : ℕ} {x₁ x₂ y₁ y₂ : Fin n → ℝ} (h₁ : IsWeaklyMajorizedBy x₁ y₁) (h₂ : IsWeaklyMajorizedBy x₂ y₂) : IsWeaklyMajorizedBy (x₁ + x₂) (y₁ + y₂)

Weak majorization is preserved by adding two weakly majorized pairs.

theorem TauCeti.IsWeaklyMajorizedBy.smul {n : ℕ} {x y : Fin n → ℝ} (h : IsWeaklyMajorizedBy x y) {c : ℝ} (hc : 0 ≤ c) : IsWeaklyMajorizedBy (c • x) (c • y)

Weak majorization is preserved by scaling both tuples by a nonnegative real.

theorem TauCeti.IsWeaklyMajorizedBy.append_zero {n : ℕ} {x y : Fin n → ℝ} (h : IsWeaklyMajorizedBy x y) (m : ℕ) : IsWeaklyMajorizedBy (Fin.append x 0) (Fin.append y 0)

Appending the same number of zeros to two tuples preserves weak majorization.

Robin Hood transfers

def TauCeti.robinHood {ι : Type u_1} [DecidableEq ι] (x : ι → ℝ) (i j : ι) (δ : ℝ) : ι → ℝ

The Robin Hood transfer of δ from coordinate i to coordinate j of x: the tuple obtained by subtracting δ from x i and adding it to x j. It is an elementary step of majorization when 0 ≤ δ ≤ x i - x j, that is, when mass moves from a larger coordinate to a smaller one so that both new values lie between x j and x i; the two coordinates may swap order.

@[simp]

theorem TauCeti.robinHood_self {ι : Type u_1} [DecidableEq ι] (x : ι → ℝ) (i : ι) (δ : ℝ) : robinHood x i i δ = x

@[simp]

theorem TauCeti.robinHood_apply_left {ι : Type u_1} [DecidableEq ι] (x : ι → ℝ) {i j : ι} (hij : i ≠ j) (δ : ℝ) : robinHood x i j δ i = x i - δ

@[simp]

theorem TauCeti.robinHood_apply_right {ι : Type u_1} [DecidableEq ι] (x : ι → ℝ) {i j : ι} (hij : i ≠ j) (δ : ℝ) : robinHood x i j δ j = x j + δ

@[simp]

theorem TauCeti.robinHood_apply_of_ne {ι : Type u_1} [DecidableEq ι] (x : ι → ℝ) {i j k : ι} (hi : k ≠ i) (hj : k ≠ j) (δ : ℝ) : robinHood x i j δ k = x k

@[simp]

theorem TauCeti.sum_robinHood {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x : ι → ℝ) (i j : ι) (δ : ℝ) : ∑ k : ι, robinHood x i j δ k = ∑ k : ι, x k

A Robin Hood transfer preserves the total sum.

@[simp]

theorem TauCeti.prefixSum_robinHood {n : ℕ} (k : ℕ) (x : Fin n → ℝ) (i j : Fin n) (δ : ℝ) : prefixSum k (robinHood x i j δ) = (prefixSum k x - if ↑i < k then δ else 0) + if ↑j < k then δ else 0

Prefix sums of a Robin Hood transfer: the transferred amount leaves the prefix sum when the source coordinate lies below the cut, and enters it when the target coordinate does.

theorem Convex.robinHood_mem {ι : Type u_1} [DecidableEq ι] {K : Set (ι → ℝ)} (hK : Convex ℝ K) {x : ι → ℝ} {i j : ι} {δ : ℝ} (hx : x ∈ K) (hswap : x ∘ ⇑(Equiv.swap i j) ∈ K) (hδ : 0 ≤ δ) (hδ' : δ ≤ x i - x j) : TauCeti.robinHood x i j δ ∈ K

Convex sets are closed under Robin Hood transfers. If a convex set contains x and the tuple obtained from x by swapping the coordinates i and j, then it contains every Robin Hood transfer of δ from i to j with 0 ≤ δ ≤ x i - x j.

def TauCeti.IsTTransform {ι : Type u_1} [DecidableEq ι] (x y : ι → ℝ) : Prop

y is a T-transform of x: it is obtained from x by one Robin Hood transfer from a coordinate to a coordinate with no larger value, followed by a permutation of the coordinates.

theorem TauCeti.IsTTransform.sum_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {x y : ι → ℝ} (h : IsTTransform x y) : ∑ k : ι, y k = ∑ k : ι, x k

A T-transform preserves the total sum.

Transfer closure

theorem TauCeti.mem_of_prefixSum_le_of_sum_eq {n : ℕ} {K : Set (Fin n → ℝ)} (hK : ∀ x ∈ K, ∀ (i j : Fin n) (δ : ℝ), 0 ≤ δ → δ ≤ x i - x j → robinHood x i j δ ∈ K) {y d : Fin n → ℝ} (hy : y ∈ K) (hd : Antitone d) (hle : ∀ (k : ℕ), prefixSum k d ≤ prefixSum k y) (hsum : ∑ i : Fin n, d i = ∑ i : Fin n, y i) : d ∈ K

Transfer closure. Let K be a set of real tuples that is closed under every Robin Hood transfer from a coordinate to one with no larger value. If K contains y, then it contains every antitone tuple d with the same total sum as y whose prefix sums are bounded by those of y. No order condition on y is needed.

When y is antitone too, the hypotheses on d say that d is majorized by y.

Symmetric convex sets

structure TauCeti.IsSymmetricConvex {ι : Type u_1} [DecidableEq ι] (K : Set (ι → ℝ)) : Prop

A set of real tuples is symmetric convex when it is convex, invariant under permutations of the coordinates, and invariant under changing the sign of one coordinate. Sublevel sets of symmetric gauges are the motivating examples.

• convex : Convex ℝ K
• comp_perm_mem (σ : Equiv.Perm ι) (x : ι → ℝ) : x ∈ K → x ∘ ⇑σ ∈ K
• update_neg_mem (x : ι → ℝ) : x ∈ K → ∀ (i : ι), Function.update x i (-x i) ∈ K

theorem TauCeti.IsSymmetricConvex.update_mem {ι : Type u_1} [DecidableEq ι] {K : Set (ι → ℝ)} {x : ι → ℝ} (hK : IsSymmetricConvex K) (hx : x ∈ K) (i : ι) {t : ℝ} (ht : |t| ≤ |x i|) : Function.update x i t ∈ K

A coordinate of a member of a symmetric convex set may be replaced by any value of no larger absolute value.

theorem TauCeti.IsSymmetricConvex.isSolid {ι : Type u_1} [DecidableEq ι] {K : Set (ι → ℝ)} [Finite ι] (hK : IsSymmetricConvex K) : LatticeOrderedAddCommGroup.IsSolid K

Symmetric convex sets are solid. A symmetric convex set containing x contains every tuple whose coordinates are bounded in absolute value by those of x.

theorem TauCeti.IsSymmetricConvex.robinHood_mem {ι : Type u_1} [DecidableEq ι] {K : Set (ι → ℝ)} {x : ι → ℝ} (hK : IsSymmetricConvex K) (hx : x ∈ K) {i j : ι} {δ : ℝ} (hδ : 0 ≤ δ) (hδ' : δ ≤ x i - x j) : robinHood x i j δ ∈ K

Symmetric convex sets are closed under Robin Hood transfers.

theorem TauCeti.IsSymmetricConvex.mem_of_isTTransform {ι : Type u_1} [DecidableEq ι] {K : Set (ι → ℝ)} {x : ι → ℝ} (hK : IsSymmetricConvex K) (hx : x ∈ K) {y : ι → ℝ} (h : IsTTransform x y) : y ∈ K

Symmetric convex sets are closed under T-transforms.

theorem TauCeti.IsSymmetricConvex.preimage_snoc {n : ℕ} {K : Set (Fin (n + 1) → ℝ)} (hK : IsSymmetricConvex K) (c : ℝ) : IsSymmetricConvex ((fun (x : Fin n → ℝ) => Fin.snoc x c) ⁻¹' K)

The section of a symmetric convex set of (n + 1)-tuples at a fixed value of the last coordinate is a symmetric convex set of n-tuples.

theorem TauCeti.IsSymmetricConvex.mem_of_prefixSum_le {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsSymmetricConvex K) {y z : Fin n → ℝ} (hy : y ∈ K) (hz : Antitone z) (hz0 : 0 ≤ z) (h : ∀ (k : ℕ), prefixSum k z ≤ prefixSum k y) : z ∈ K

Transfer descent. A symmetric convex set containing a tuple y contains every antitone nonnegative tuple z whose prefix sums are bounded by those of y. No order or sign condition on y is needed.

theorem TauCeti.IsWeaklyMajorizedBy.mem {n : ℕ} {K : Set (Fin n → ℝ)} {x y : Fin n → ℝ} (h : IsWeaklyMajorizedBy x y) (hK : IsSymmetricConvex K) (hy : y ∈ K) : x ∈ K

Weak majorization descends into symmetric convex sets.

Symmetric gauges

structure Seminorm.IsSymmetricGauge {ι : Type u_1} [DecidableEq ι] (p : Seminorm ℝ (ι → ℝ)) : Prop

A seminorm p on real tuples is a symmetric gauge when it is invariant under permutations of the coordinates and under changing the sign of one coordinate.

• map_comp_perm (σ : Equiv.Perm ι) (x : ι → ℝ) : p (x ∘ ⇑σ) = p x
• map_update_neg (x : ι → ℝ) (i : ι) : p (Function.update x i (-x i)) = p x

theorem Seminorm.IsSymmetricGauge.isSymmetricConvex_setOf_le {ι : Type u_1} [DecidableEq ι] {p : Seminorm ℝ (ι → ℝ)} (hp : p.IsSymmetricGauge) (c : ℝ) : TauCeti.IsSymmetricConvex {x : ι → ℝ | p x ≤ c}

The sublevel sets of a symmetric gauge are symmetric convex.

theorem Seminorm.isSymmetricGauge_normSeminorm {ι : Type u_1} [DecidableEq ι] [Fintype ι] : (normSeminorm ℝ (ι → ℝ)).IsSymmetricGauge

The sup norm on real tuples is a symmetric gauge.

theorem Seminorm.isSymmetricGauge_piLp {ι : Type u_1} [DecidableEq ι] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] : ((normSeminorm ℝ (PiLp p fun (x : ι) => ℝ)).comp ↑(WithLp.linearEquiv p ℝ (ι → ℝ)).symm).IsSymmetricGauge

For 1 ≤ p ≤ ∞, the ℓᵖ norm x ↦ (∑ᵢ |xᵢ|ᵖ)^(1/p) on real tuples (the sup norm for p = ∞), read through WithLp.toLp, is a symmetric gauge.

theorem Seminorm.IsSymmetricGauge.apply_le_of_abs_le {ι : Type u_1} [DecidableEq ι] [Finite ι] {p : Seminorm ℝ (ι → ℝ)} (hp : p.IsSymmetricGauge) {x y : ι → ℝ} (h : |x| ≤ |y|) : p x ≤ p y

A symmetric gauge is monotone in the absolute values of the coordinates: if |x i| ≤ |y i| for every i, then p x ≤ p y.

theorem Seminorm.IsSymmetricGauge.map_abs {ι : Type u_1} [DecidableEq ι] [Finite ι] {p : Seminorm ℝ (ι → ℝ)} (hp : p.IsSymmetricGauge) (x : ι → ℝ) : p |x| = p x

A symmetric gauge takes the same value at a tuple and at its coordinatewise absolute value.

theorem Seminorm.IsSymmetricGauge.comp_funLeft {ι : Type u_1} [DecidableEq ι] {κ : Type u_2} [DecidableEq κ] {p : Seminorm ℝ (ι → ℝ)} (hp : p.IsSymmetricGauge) (e : ι ≃ κ) : (p.comp (LinearMap.funLeft ℝ ℝ ⇑e)).IsSymmetricGauge

Reindexing the coordinates along an equivalence preserves symmetric gauges.

theorem Seminorm.IsSymmetricGauge.ext_of_antitone {n : ℕ} {p q : Seminorm ℝ (Fin n → ℝ)} (hp : p.IsSymmetricGauge) (hq : q.IsSymmetricGauge) (h : ∀ (x : Fin n → ℝ), Antitone x → 0 ≤ x → p x = q x) : p = q

Two symmetric gauges on n-tuples agree as soon as they agree on the nonincreasing nonnegative tuples: every tuple is carried to one of these by changing signs and permuting its coordinates.

theorem Seminorm.IsSymmetricGauge.apply_le_of_prefixSum_le {n : ℕ} {p : Seminorm ℝ (Fin n → ℝ)} (hp : p.IsSymmetricGauge) {y z : Fin n → ℝ} (hz : Antitone z) (hz0 : 0 ≤ z) (h : ∀ (k : ℕ), TauCeti.prefixSum k z ≤ TauCeti.prefixSum k y) : p z ≤ p y

Symmetric gauges are monotone for prefix-sum domination. If z is antitone and nonnegative and its prefix sums are bounded by those of y, then p z ≤ p y.

theorem TauCeti.IsWeaklyMajorizedBy.apply_le {n : ℕ} {x y : Fin n → ℝ} (h : IsWeaklyMajorizedBy x y) {p : Seminorm ℝ (Fin n → ℝ)} (hp : p.IsSymmetricGauge) : p x ≤ p y

Symmetric gauges are monotone for weak majorization.