Weak majorization and the Hardy–Littlewood–Pólya transfer lemma

The combinatorial engine underlying every unitarily invariant norm inequality in this development, isolated from the operator theory that consumes it.

A T-transform (Hardy–Littlewood–Pólya; also called a Robin Hood operation) replaces a vector by a convex combination of itself with one of its transpositions. Concretely, moving δ from a larger coordinate j down to a smaller coordinate l — FiniteVector.transfer — is such a combination. The transfer lemma FiniteVector.exists_isTTransform_of_not_forall_le says that a single T-transform always makes progress: given prefix-sum domination z ≺w q that is not yet coordinatewise domination, some T-transform of q still dominates z in prefix sums while agreeing with z in strictly more coordinates. Iterating it is IsSymmetricConvex.mem_of_prefixSum_le, the transfer descent.

Main definitions

• FiniteVector.prefixSum k x — the sum of the first k coordinates of x : Fin n → ℝ.
• FiniteVector.WeaklyMajorized x y — weak majorization of vectors already presented in decreasing nonnegative order: every prefix sum of x is at most that of y.
• FiniteVector.transfer q j l δ — the elementary transfer of δ from coordinate j to coordinate l.
• FiniteVector.IsTTransform y q — q is a convex combination of y with a transposition of y.
• FiniteVector.IsSymmetricConvex K — K is convex, transposition-closed, and closed under flipping the sign of a single coordinate. These are exactly the closure properties the descent consumes.
• FiniteSymmetricGauge n — a subadditive, absolutely homogeneous, permutation-invariant, sign-flip-invariant function on Fin n → ℝ.

Main results

• FiniteVector.exists_isTTransform_of_not_forall_le — the transfer lemma.
• FiniteVector.IsSymmetricConvex.mem_of_prefixSum_le — the transfer descent: a symmetric-convex set containing y contains every antitone nonnegative z whose prefix sums are dominated by those of y.
• FiniteSymmetricGauge.le_of_prefixSum_le and FiniteSymmetricGauge.mono_weaklyMajorized — the same statement for a gauge, obtained by applying the descent to the sublevel set {x | Φ x ≤ Φ y}, which FiniteSymmetricGauge.isSymmetricConvex_sublevel shows is symmetric-convex.

Nothing here needs a separation theorem, Birkhoff's theorem on doubly stochastic matrices, or a majorization completion: total-sum equality is never assumed, and each descent step costs one convexity application and one closure property.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original modules: ForTauCeti.Analysis.Normed.FiniteLpGauge (the FiniteVector vocabulary, FiniteSymmetricGauge, and its majorization monotonicity), ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm and ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Majorization (two further copies of the same descent, now deleted in favour of this one).
• Extraction class: split and generalized. The moved declarations keep their names and statements; the descent itself was restated for a symmetric-convex set, which is the common generalization of the three copies, and factored through the T-transform vocabulary.
• Original authors / copyright: Jon Crall, GPT-5.6 Thinking, Claude Fable 5, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib.

Prefix sums

def TauCeti.FiniteVector.prefixSum {n : ℕ} (k : ℕ) (x : Fin n → ℝ) : ℝ

Sum of the first k coordinates of a finite vector. For k ≥ n this is its full sum.

Equations

• TauCeti.FiniteVector.prefixSum k x = ∑ i : Fin n with ↑i < k, x i

@[simp]

theorem TauCeti.FiniteVector.prefixSum_zero {n : ℕ} (k : ℕ) : prefixSum k 0 = 0

Prefix sums of the zero vector vanish.

@[simp]

theorem TauCeti.FiniteVector.prefixSum_add {n : ℕ} (k : ℕ) (x y : Fin n → ℝ) : prefixSum k (x + y) = prefixSum k x + prefixSum k y

Prefix sums are additive.

@[simp]

theorem TauCeti.FiniteVector.prefixSum_smul {n : ℕ} (k : ℕ) (c : ℝ) (x : Fin n → ℝ) : prefixSum k (c • x) = c * prefixSum k x

Prefix sums are homogeneous.

theorem TauCeti.FiniteVector.prefixSum_eq_full_sum_of_le {n : ℕ} (x : Fin n → ℝ) {k : ℕ} (hk : n ≤ k) : prefixSum k x = ∑ i : Fin n, x i

Prefix sums stabilize after the vector length.

Weak majorization

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

Weak majorization for vectors already presented in decreasing, nonnegative order.

• left_antitone : Antitone x
• right_antitone : Antitone y
• left_nonneg (i : Fin n) : 0 ≤ x i
• right_nonneg (i : Fin n) : 0 ≤ y i
• prefix_le (k : ℕ) : prefixSum k x ≤ prefixSum k y

theorem TauCeti.FiniteVector.WeaklyMajorized.refl {n : ℕ} {x : Fin n → ℝ} (hxanti : Antitone x) (hx0 : ∀ (i : Fin n), 0 ≤ x i) : WeaklyMajorized x x

Weak majorization is reflexive on decreasing nonnegative vectors.

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

Weak majorization is transitive.

theorem TauCeti.FiniteVector.WeaklyMajorized.of_pointwise {n : ℕ} {x y : Fin n → ℝ} (hxanti : Antitone x) (hyanti : Antitone y) (hx0 : ∀ (i : Fin n), 0 ≤ x i) (hy0 : ∀ (i : Fin n), 0 ≤ y i) (hxy : ∀ (i : Fin n), x i ≤ y i) : WeaklyMajorized x y

Coordinatewise domination implies weak majorization when both vectors are already decreasing and nonnegative.

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

Weak majorization is compatible with vector addition.

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

Nonnegative scaling preserves weak majorization.

theorem TauCeti.FiniteVector.WeaklyMajorized.sum_le {n : ℕ} {x y : Fin n → ℝ} (h : WeaklyMajorized x y) : ∑ i : Fin n, x i ≤ ∑ i : Fin n, y i

The full-sum consequence of weak majorization.

Zero padding

def TauCeti.FiniteVector.zeroPadRight {n m : ℕ} (x : Fin n → ℝ) : Fin (n + m) → ℝ

Right zero-padding from length n to length n + m.

Equations

• TauCeti.FiniteVector.zeroPadRight x i = if hi : ↑i < n then x ⟨↑i, hi⟩ else 0

@[simp]

theorem TauCeti.FiniteVector.zeroPadRight_left {n m : ℕ} (x : Fin n → ℝ) (i : Fin n) : zeroPadRight x (Fin.castAdd m i) = x i

Zero padding leaves the original coordinates alone.

@[simp]

theorem TauCeti.FiniteVector.zeroPadRight_right {n m : ℕ} (x : Fin n → ℝ) (i : Fin m) : zeroPadRight x (Fin.natAdd n i) = 0

The padded coordinates are zero.

theorem TauCeti.FiniteVector.prefixSum_zeroPadRight {n m : ℕ} (k : ℕ) (x : Fin n → ℝ) : prefixSum k (zeroPadRight x) = prefixSum k x

Zero padding preserves every prefix sum.

theorem TauCeti.FiniteVector.antitone_zeroPadRight {n m : ℕ} {x : Fin n → ℝ} (hxanti : Antitone x) (hx0 : ∀ (i : Fin n), 0 ≤ x i) : Antitone (zeroPadRight x)

A decreasing nonnegative vector remains decreasing after appending zeros.

theorem TauCeti.FiniteVector.zeroPadRight_nonneg {n m : ℕ} {x : Fin n → ℝ} (hx0 : ∀ (i : Fin n), 0 ≤ x i) (i : Fin (n + m)) : 0 ≤ zeroPadRight x i

Zero padding preserves nonnegativity.

theorem TauCeti.FiniteVector.WeaklyMajorized.zeroPadRight {n m : ℕ} {x y : Fin n → ℝ} (h : WeaklyMajorized x y) : WeaklyMajorized (FiniteVector.zeroPadRight x) (FiniteVector.zeroPadRight y)

Appending a common zero tail preserves weak majorization.

T-transforms

def TauCeti.FiniteVector.transfer {n : ℕ} (q : Fin n → ℝ) (j l : Fin n) (δ : ℝ) : Fin n → ℝ

The elementary transfer of δ from coordinate j to coordinate l: the Hardy–Littlewood–Pólya "Robin Hood" operation, which takes δ from the richer coordinate and gives it to the poorer one.

Equations

• TauCeti.FiniteVector.transfer q j l δ = Function.update (Function.update q j (q j - δ)) l (q l + δ)

theorem TauCeti.FiniteVector.transfer_apply_left {n : ℕ} {q : Fin n → ℝ} {j l : Fin n} (hjl : j ≠ l) (δ : ℝ) : transfer q j l δ j = q j - δ

At the donor coordinate the transfer removes δ. Needs j ≠ l, since a self-transfer would have the receiving update overwrite the donating one.

theorem TauCeti.FiniteVector.transfer_apply_right {n : ℕ} (q : Fin n → ℝ) (j l : Fin n) (δ : ℝ) : transfer q j l δ l = q l + δ

At the receiving coordinate the transfer adds δ.

theorem TauCeti.FiniteVector.transfer_apply_of_ne {n : ℕ} {q : Fin n → ℝ} {i j l : Fin n} (hij : i ≠ j) (hil : i ≠ l) (δ : ℝ) : transfer q j l δ i = q i

A transfer leaves every coordinate other than the two it moves mass between unchanged.

@[simp]

theorem TauCeti.FiniteVector.transfer_zero {n : ℕ} (q : Fin n → ℝ) (j l : Fin n) : transfer q j l 0 = q

A transfer of nothing is the identity.

theorem TauCeti.FiniteVector.prefixSum_transfer {n : ℕ} {q : Fin n → ℝ} {j l : Fin n} (hjl : j ≠ l) (δ : ℝ) (k : ℕ) : prefixSum k (transfer q j l δ) = (prefixSum k q - if ↑j < k then δ else 0) + if ↑l < k then δ else 0

The prefix sums of a transfer: the moved mass leaves the prefix once it passes j and returns once it passes l. In particular a transfer preserves every prefix sum that contains both coordinates or neither.

def TauCeti.FiniteVector.IsTTransform {n : ℕ} (y q : Fin n → ℝ) : Prop

q is a T-transform of y: a convex combination of y with one of its transpositions. This is the elementary move of Hardy–Littlewood–Pólya majorization theory; isTTransform_transfer exhibits transfer as one.

Equations

• TauCeti.FiniteVector.IsTTransform y q = ∃ (j : Fin n) (l : Fin n) (c : ℝ), 0 ≤ c ∧ c ≤ 1 ∧ q = (1 - c) • y + c • y ∘ ⇑(Equiv.swap j l)

theorem TauCeti.FiniteVector.isTTransform_transfer {n : ℕ} {q : Fin n → ℝ} {j l : Fin n} (hjl : j ≠ l) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ : δ ≤ q j - q l) : IsTTransform q (transfer q j l δ)

The elementary transfer is a T-transform. Moving δ ≥ 0 from j to l without overshooting (δ ≤ q j - q l) is averaging q with its (j l)-transposition.

The transfer lemma

theorem TauCeti.FiniteVector.exists_isTTransform_of_not_forall_le {n : ℕ} {z q : Fin n → ℝ} (hz : Antitone z) (hz0 : ∀ (i : Fin n), 0 ≤ z i) (hq0 : ∀ (i : Fin n), 0 ≤ q i) (hpre : ∀ (k : ℕ), prefixSum k z ≤ prefixSum k q) (hnot : ¬∀ (i : Fin n), z i ≤ q i) : ∃ (q' : Fin n → ℝ), IsTTransform q q' ∧ (∀ (i : Fin n), 0 ≤ q' i) ∧ (∀ (k : ℕ), prefixSum k z ≤ prefixSum k q') ∧ {i : Fin n | z i ≠ q' i}.card < {i : Fin n | z i ≠ q i}.card

The Hardy–Littlewood–Pólya transfer lemma. Let z be antitone and nonnegative and let q be nonnegative with every prefix sum of z dominated by that of q. If q does not already dominate z coordinatewise, then a single T-transform of q still dominates z in prefix sums, is still nonnegative, and agrees with z in strictly more coordinates.

This is the whole content of the majorization descent: everything below iterates it. The transform moves mass from the least index j where q is strictly above z down to the least index l where q falls strictly below z, stopping as soon as either coordinate meets z.

Symmetric-convex sets and the transfer descent

structure TauCeti.FiniteVector.IsSymmetricConvex {n : ℕ} (K : Set (Fin n → ℝ)) : Prop

A set of finite real vectors is symmetric-convex when it is convex, closed under coordinate transpositions, and closed under flipping the sign of a single coordinate.

These are exactly the properties the transfer descent consumes, and exactly the properties a sublevel set of a symmetric gauge has (FiniteSymmetricGauge.isSymmetricConvex_sublevel).

• convex : Convex ℝ K
• swap_mem (y : Fin n → ℝ) : y ∈ K → ∀ (j l : Fin n), y ∘ ⇑(Equiv.swap j l) ∈ K
• neg_single_mem (y : Fin n → ℝ) : y ∈ K → ∀ (j : Fin n), Function.update y j (-y j) ∈ K

theorem TauCeti.FiniteVector.IsSymmetricConvex.mem_of_isTTransform {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsSymmetricConvex K) {y q : Fin n → ℝ} (hy : y ∈ K) (h : IsTTransform y q) : q ∈ K

A symmetric-convex set is closed under T-transforms.

theorem TauCeti.FiniteVector.IsSymmetricConvex.update_mem {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsSymmetricConvex K) {q : Fin n → ℝ} (hq : q ∈ K) (j : Fin n) {t : ℝ} (ht : |t| ≤ q j) : Function.update q j t ∈ K

Shrinking one coordinate of q ∈ K in absolute value stays in K: the update is the midpoint-style convex combination of q with its j-th sign flip.

theorem TauCeti.FiniteVector.IsSymmetricConvex.mem_of_forall_le {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsSymmetricConvex K) {z q : Fin n → ℝ} (hz0 : ∀ (i : Fin n), 0 ≤ z i) (hzq : ∀ (i : Fin n), z i ≤ q i) (hq : q ∈ K) : z ∈ K

Coordinatewise descent. A symmetric-convex set containing q contains every nonnegative vector below q.

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

The Hardy–Littlewood–Pólya transfer descent. If z is antitone and nonnegative, y is nonnegative, and every prefix sum of z is dominated by the corresponding prefix sum of y, then every symmetric-convex set containing y contains z.

The proof iterates the transfer lemma exists_isTTransform_of_not_forall_le: each T-transform stays inside K, keeps the prefix domination, and strictly reduces the number of coordinates where z and the current vector disagree. When no disagreement above z is left, the coordinatewise descent finishes.

No total-sum equality is assumed, and no majorization completion, separation theorem, or Birkhoff decomposition is used.

theorem TauCeti.FiniteVector.IsSymmetricConvex.mem_of_weaklyMajorized {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsSymmetricConvex K) {z y : Fin n → ℝ} (h : WeaklyMajorized z y) (hy : y ∈ K) : z ∈ K

The transfer descent, phrased with WeaklyMajorized.

Finite symmetric gauges

structure TauCeti.FiniteSymmetricGauge (n : ℕ) : Type

Algebraic interface for a finite symmetric gauge. These are precisely the properties used by the T-transform proof of weak-majorization monotonicity.

• toFun : (Fin n → ℝ) → ℝ

  The real-valued gauge on finite coordinate vectors.

• add_le' (x y : Fin n → ℝ) : self.toFun (x + y) ≤ self.toFun x + self.toFun y
• real_smul' (c : ℝ) (x : Fin n → ℝ) : self.toFun (c • x) = |c| * self.toFun x
• perm' (x : Fin n → ℝ) (π : Equiv.Perm (Fin n)) : self.toFun (x ∘ ⇑π) = self.toFun x
• neg_single' (x : Fin n → ℝ) (j : Fin n) : self.toFun (Function.update x j (-x j)) = self.toFun x

@[instance_reducible]

instance TauCeti.FiniteSymmetricGauge.instCoeFunForallForallFinReal {n : ℕ} : CoeFun (FiniteSymmetricGauge n) fun (x : FiniteSymmetricGauge n) => (Fin n → ℝ) → ℝ

Apply a finite symmetric gauge directly to a vector, writing Φ x for Φ.toFun x.

Equations

• TauCeti.FiniteSymmetricGauge.instCoeFunForallForallFinReal = { coe := TauCeti.FiniteSymmetricGauge.toFun }

theorem TauCeti.FiniteSymmetricGauge.add_le {n : ℕ} (Φ : FiniteSymmetricGauge n) (x y : Fin n → ℝ) : Φ.toFun (x + y) ≤ Φ.toFun x + Φ.toFun y

Subadditivity of a finite symmetric gauge.

theorem TauCeti.FiniteSymmetricGauge.real_smul {n : ℕ} (Φ : FiniteSymmetricGauge n) (c : ℝ) (x : Fin n → ℝ) : Φ.toFun (c • x) = |c| * Φ.toFun x

Absolute homogeneity of a finite symmetric gauge.

theorem TauCeti.FiniteSymmetricGauge.perm {n : ℕ} (Φ : FiniteSymmetricGauge n) (x : Fin n → ℝ) (π : Equiv.Perm (Fin n)) : Φ.toFun (x ∘ ⇑π) = Φ.toFun x

A finite symmetric gauge is invariant under permuting coordinates -- the symmetric half of the name.

theorem TauCeti.FiniteSymmetricGauge.neg_single {n : ℕ} (Φ : FiniteSymmetricGauge n) (x : Fin n → ℝ) (j : Fin n) : Φ.toFun (Function.update x j (-x j)) = Φ.toFun x

A finite symmetric gauge is invariant under flipping the sign of a single coordinate. With perm this gives invariance under all signed permutations, which is what makes the sublevel sets symmetric-convex.

theorem TauCeti.FiniteSymmetricGauge.isSymmetricConvex_sublevel {n : ℕ} (Φ : FiniteSymmetricGauge n) (r : ℝ) : FiniteVector.IsSymmetricConvex {x : Fin n → ℝ | Φ.toFun x ≤ r}

Every sublevel set of a finite symmetric gauge is symmetric-convex. This is the bridge that lets the whole majorization theory be proved once, for sets, and read off for gauges: convexity is subadditivity plus absolute homogeneity, and the two closure properties are the gauge's permutation and sign-flip invariance.

theorem TauCeti.FiniteSymmetricGauge.update_le {n : ℕ} (Φ : FiniteSymmetricGauge n) {y : Fin n → ℝ} {j : Fin n} {t : ℝ} (ht : |t| ≤ y j) : Φ.toFun (Function.update y j t) ≤ Φ.toFun y

Shrinking one coordinate of y (in absolute value) does not increase the gauge: update y j t with |t| ≤ y j is a convex combination of y and its j-th sign flip.

theorem TauCeti.FiniteSymmetricGauge.mono {n : ℕ} (Φ : FiniteSymmetricGauge n) {x y : Fin n → ℝ} (hx0 : ∀ (i : Fin n), 0 ≤ x i) (hxy : ∀ (i : Fin n), x i ≤ y i) : Φ.toFun x ≤ Φ.toFun y

Coordinatewise monotonicity of the gauge on nonnegative vectors.

theorem TauCeti.FiniteSymmetricGauge.le_of_prefixSum_le {n : ℕ} (Φ : FiniteSymmetricGauge n) {z y : Fin n → ℝ} (hz_anti : Antitone z) (hz0 : ∀ (i : Fin n), 0 ≤ z i) (hy0 : ∀ (i : Fin n), 0 ≤ y i) (hpre : ∀ (k : ℕ), ∑ i : Fin n with ↑i < k, z i ≤ ∑ i : Fin n with ↑i < k, y i) : Φ.toFun z ≤ Φ.toFun y

The T-transform descent on the gauge — the engine of Fan dominance. If z is antitone and nonnegative, y is nonnegative, and every prefix sum of z is dominated by the corresponding prefix sum of y, then Φ z ≤ Φ y.

An instance of FiniteVector.IsSymmetricConvex.mem_of_prefixSum_le at the sublevel set {x | Φ x ≤ Φ y}.

theorem TauCeti.FiniteSymmetricGauge.mono_weaklyMajorized {n : ℕ} (Φ : FiniteSymmetricGauge n) {x y : Fin n → ℝ} (h : FiniteVector.WeaklyMajorized x y) : Φ.toFun x ≤ Φ.toFun y

Every finite symmetric gauge is monotone under weak majorization.

Antitone rearrangement

Tuple.sort produces a monotone rearrangement. Several results downstream -- realizing a sequence as the approximation numbers of a diagonal operator, and the block-sum statement that the sequence of a block-diagonal sum is the decreasing rearrangement of the union -- need the antitone one instead.

Composing the sorting permutation with Fin.rev supplies it, and a symmetric gauge cannot tell the difference, since permutation invariance is one of its axioms.

def TauCeti.FiniteSymmetricGauge.revPerm (n : ℕ) : Equiv.Perm (Fin n)

Fin.rev as a permutation: it is an involution.

Equations

• TauCeti.FiniteSymmetricGauge.revPerm n = Function.Involutive.toPerm Fin.rev ⋯

@[simp]

theorem TauCeti.FiniteSymmetricGauge.revPerm_apply {n : ℕ} (i : Fin n) : (revPerm n) i = i.rev

revPerm acts as Fin.rev.

noncomputable def TauCeti.FiniteSymmetricGauge.antitoneSortPerm {n : ℕ} (f : Fin n → ℝ) : Equiv.Perm (Fin n)

The permutation putting a tuple into antitone order: sort, then reverse.

Equations

• TauCeti.FiniteSymmetricGauge.antitoneSortPerm f = Equiv.trans (TauCeti.FiniteSymmetricGauge.revPerm n) (Tuple.sort f)

theorem TauCeti.FiniteSymmetricGauge.antitone_comp_antitoneSortPerm {n : ℕ} (f : Fin n → ℝ) : Antitone (f ∘ ⇑(antitoneSortPerm f))

The rearrangement is antitone.

Tuple.monotone_sort makes f ∘ sort f monotone, and Fin.rev is strictly antitone, so the composite reverses order.

theorem TauCeti.FiniteSymmetricGauge.apply_antitoneSortPerm {n : ℕ} (Φ : FiniteSymmetricGauge n) (f : Fin n → ℝ) : Φ.toFun (f ∘ ⇑(antitoneSortPerm f)) = Φ.toFun f

A finite symmetric gauge does not see the rearrangement.