Symmetric gauges on sequences

A symmetric gauge (a symmetric norming function in the terminology of Gohberg and Krein) is a function Φ on finitely supported nonnegative sequences a : ℕ →₀ ℝ≥0 that is subadditive, positively homogeneous, invariant under permutations of the indices, monotone in the termwise order, and normalized by Φ (single 0 1) = 1. Applied to the sequence of approximation numbers of an operator, a symmetric gauge produces the norm of a symmetric operator ideal; the ℓᵖ gauges produce the Schatten classes.

Every symmetric gauge lies between the supremum and the sum of the sequence, ⨆ n, a n ≤ Φ a ≤ ∑ n, a n. It extends to arbitrary sequences a : ℕ → ℝ≥0∞ as the supremum of Φ b over the finitely supported b dominated by a. The extension is total, lies between the supremum and the sum of the sequence, and keeps the monotonicity, homogeneity and subadditivity of Φ, as well as its permutation invariance. These laws feed the ideal-norm properties of the induced gauge on operators. For a finite-valued sequence the extension is the supremum of Φ along the initial truncations of the sequence, with no monotonicity hypothesis on the sequence.

The finite counterpart, a permutation- and sign-invariant seminorm on ι → ℝ, is Seminorm.IsSymmetricGauge in TauCeti.Analysis.Convex.Majorization. Restricting Φ to the first n coordinates gives such a seminorm on Fin n → ℝ, so the transfer descent proved there applies: symmetric gauges are monotone for weak majorization. If a is antitone and every partial sum of a is at most the corresponding partial sum of b, then Φ∞ a ≤ Φ∞ b. Applied to approximation numbers, this turns Ky Fan dominance into domination for every induced gauge.

Main definitions

• TauCeti.SymmetricGauge: symmetric gauges on finitely supported nonnegative sequences.
• TauCeti.SymmetricGauge.extend: the extension Φ∞ of a symmetric gauge to ℕ → ℝ≥0∞.
• TauCeti.SymmetricGauge.supGauge: the supremum ⨆ n, a n, the least symmetric gauge.
• TauCeti.SymmetricGauge.finSeminorm: the restriction of a symmetric gauge to the first n coordinates, as a seminorm on Fin n → ℝ.

Main results

• TauCeti.SymmetricGauge.iSup_le_apply, TauCeti.SymmetricGauge.apply_le_sum: ⨆ n, a n ≤ Φ a ≤ ∑ n, a n.
• TauCeti.SymmetricGauge.extend_coe: the extension agrees with Φ on finitely supported sequences.
• TauCeti.SymmetricGauge.iSup_le_extend, TauCeti.SymmetricGauge.extend_le_tsum: ⨆ n, a n ≤ Φ∞ a ≤ ∑' n, a n.
• TauCeti.SymmetricGauge.extend_coe_eq_iSup_indicator: the truncation formula for finite-valued sequences.
• TauCeti.SymmetricGauge.extend_mono, TauCeti.SymmetricGauge.extend_smul, TauCeti.SymmetricGauge.extend_add_le, TauCeti.SymmetricGauge.extend_comp_perm: the extension is monotone, homogeneous, subadditive and permutation invariant.
• TauCeti.SymmetricGauge.isSymmetricGauge_finSeminorm: the restriction to n coordinates is a symmetric gauge on Fin n → ℝ.
• TauCeti.SymmetricGauge.apply_le_apply_of_forall_sum_le, TauCeti.SymmetricGauge.extend_le_extend_of_forall_sum_le: symmetric gauges and their extensions are monotone for weak majorization.

References

• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators in Hilbert Space, Translations of Mathematical Monographs 18, AMS (1969), Chapter III.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §IV.1.
• B. Simon, Trace Ideals and Their Applications, 2nd ed., Mathematical Surveys and Monographs 120, AMS (2005).

structure TauCeti.SymmetricGauge : Type

A symmetric gauge (symmetric norming function): a subadditive, positively homogeneous, permutation-invariant and monotone function on finitely supported nonnegative sequences, normalized by taking the value 1 on the first basis vector.

• toFun : (ℕ →₀ NNReal) → NNReal

  The underlying function on finitely supported nonnegative sequences.

• map_add_le' (a b : ℕ →₀ NNReal) : self.toFun (a + b) ≤ self.toFun a + self.toFun b

  Subadditivity.

• map_smul' (c : NNReal) (a : ℕ →₀ NNReal) : self.toFun (c • a) = c * self.toFun a

  Positive homogeneity.

• map_equivMapDomain' (σ : Equiv.Perm ℕ) (a : ℕ →₀ NNReal) : self.toFun (Finsupp.equivMapDomain σ a) = self.toFun a

  Invariance under permutations of the indices.

• monotone' : Monotone self.toFun

  Monotonicity in the termwise order.

• map_single_zero_one' : self.toFun (Finsupp.single 0 1) = 1

  Normalization on the first basis vector.

@[instance_reducible]

instance TauCeti.SymmetricGauge.instFunLikeFinsuppNatNNReal : FunLike SymmetricGauge (ℕ →₀ NNReal) NNReal

theorem TauCeti.SymmetricGauge.ext {Φ Ψ : SymmetricGauge} (h : ∀ (a : ℕ →₀ NNReal), Φ a = Ψ a) : Φ = Ψ

theorem TauCeti.SymmetricGauge.ext_iff {Φ Ψ : SymmetricGauge} : Φ = Ψ ↔ ∀ (a : ℕ →₀ NNReal), Φ a = Ψ a

@[simp]

theorem TauCeti.SymmetricGauge.toFun_eq_coe (Φ : SymmetricGauge) : Φ.toFun = ⇑Φ

@[simp]

theorem TauCeti.SymmetricGauge.coe_mk (f : (ℕ →₀ NNReal) → NNReal) (h₁ : ∀ (a b : ℕ →₀ NNReal), f (a + b) ≤ f a + f b) (h₂ : ∀ (c : NNReal) (a : ℕ →₀ NNReal), f (c • a) = c * f a) (h₃ : ∀ (σ : Equiv.Perm ℕ) (a : ℕ →₀ NNReal), f (Finsupp.equivMapDomain σ a) = f a) (h₄ : Monotone f) (h₅ : f (Finsupp.single 0 1) = 1) : ⇑{ toFun := f, map_add_le' := h₁, map_smul' := h₂, map_equivMapDomain' := h₃, monotone' := h₄, map_single_zero_one' := h₅ } = f

theorem TauCeti.SymmetricGauge.map_add_le (Φ : SymmetricGauge) (a b : ℕ →₀ NNReal) : Φ (a + b) ≤ Φ a + Φ b

@[simp]

theorem TauCeti.SymmetricGauge.map_smul (Φ : SymmetricGauge) (c : NNReal) (a : ℕ →₀ NNReal) : Φ (c • a) = c * Φ a

@[simp]

theorem TauCeti.SymmetricGauge.map_equivMapDomain (Φ : SymmetricGauge) (σ : Equiv.Perm ℕ) (a : ℕ →₀ NNReal) : Φ (Finsupp.equivMapDomain σ a) = Φ a

theorem TauCeti.SymmetricGauge.monotone (Φ : SymmetricGauge) : Monotone ⇑Φ

theorem TauCeti.SymmetricGauge.mono (Φ : SymmetricGauge) {a b : ℕ →₀ NNReal} (h : a ≤ b) : Φ a ≤ Φ b

theorem TauCeti.SymmetricGauge.map_single_zero_one (Φ : SymmetricGauge) : Φ (Finsupp.single 0 1) = 1

@[simp]

theorem TauCeti.SymmetricGauge.map_zero (Φ : SymmetricGauge) : Φ 0 = 0

@[simp]

theorem TauCeti.SymmetricGauge.map_single (Φ : SymmetricGauge) (n : ℕ) (c : NNReal) : Φ (Finsupp.single n c) = c

A symmetric gauge takes the value c on every sequence with a single nonzero term c.

theorem TauCeti.SymmetricGauge.iSup_le_apply (Φ : SymmetricGauge) (a : ℕ →₀ NNReal) : ⨆ (n : ℕ), a n ≤ Φ a

The lower end of the scale: a symmetric gauge dominates the supremum of the sequence.

theorem TauCeti.SymmetricGauge.apply_le_sum (Φ : SymmetricGauge) (a : ℕ →₀ NNReal) : Φ a ≤ ∑ n ∈ a.support, a n

The upper end of the scale: a symmetric gauge is dominated by the sum of the sequence.

The extension to arbitrary sequences

noncomputable def TauCeti.SymmetricGauge.extend (Φ : SymmetricGauge) (a : ℕ → ENNReal) : ENNReal

The extension Φ∞ of a symmetric gauge to sequences in ℝ≥0∞: the supremum of Φ b over the finitely supported sequences b dominated termwise by a.

theorem TauCeti.SymmetricGauge.extend_def (Φ : SymmetricGauge) (a : ℕ → ENNReal) : Φ.extend a = ⨆ (b : ℕ →₀ NNReal), ⨆ (_ : ∀ (n : ℕ), ↑(b n) ≤ a n), ↑(Φ b)

theorem TauCeti.SymmetricGauge.apply_le_extend (Φ : SymmetricGauge) {a : ℕ → ENNReal} {b : ℕ →₀ NNReal} (hb : ∀ (n : ℕ), ↑(b n) ≤ a n) : ↑(Φ b) ≤ Φ.extend a

theorem TauCeti.SymmetricGauge.extend_le_iff (Φ : SymmetricGauge) {a : ℕ → ENNReal} {c : ENNReal} : Φ.extend a ≤ c ↔ ∀ (b : ℕ →₀ NNReal), (∀ (n : ℕ), ↑(b n) ≤ a n) → ↑(Φ b) ≤ c

@[simp]

theorem TauCeti.SymmetricGauge.extend_coe (Φ : SymmetricGauge) (a : ℕ →₀ NNReal) : (Φ.extend fun (n : ℕ) => ↑(a n)) = ↑(Φ a)

On finitely supported sequences the extension is the gauge itself.

theorem TauCeti.SymmetricGauge.extend_mono (Φ : SymmetricGauge) : Monotone Φ.extend

The extension is monotone in the termwise order.

theorem TauCeti.SymmetricGauge.extend_le_extend (Φ : SymmetricGauge) {a b : ℕ → ENNReal} (h : a ≤ b) : Φ.extend a ≤ Φ.extend b

theorem TauCeti.SymmetricGauge.iSup_le_extend (Φ : SymmetricGauge) (a : ℕ → ENNReal) : ⨆ (n : ℕ), a n ≤ Φ.extend a

The extension dominates the supremum of the sequence.

theorem TauCeti.SymmetricGauge.extend_le_tsum (Φ : SymmetricGauge) (a : ℕ → ENNReal) : Φ.extend a ≤ ∑' (n : ℕ), a n

The extension is dominated by the sum of the sequence.

@[simp]

theorem TauCeti.SymmetricGauge.extend_zero (Φ : SymmetricGauge) : Φ.extend 0 = 0

@[simp]

theorem TauCeti.SymmetricGauge.extend_eq_zero_iff (Φ : SymmetricGauge) {a : ℕ → ENNReal} : Φ.extend a = 0 ↔ a = 0

The extension vanishes exactly on the zero sequence.

@[simp]

theorem TauCeti.SymmetricGauge.extend_comp_perm (Φ : SymmetricGauge) (σ : Equiv.Perm ℕ) (a : ℕ → ENNReal) : Φ.extend (a ∘ ⇑σ) = Φ.extend a

The extension is invariant under permutations of the indices.

theorem TauCeti.SymmetricGauge.extend_coe_eq_iSup_indicator (Φ : SymmetricGauge) (a : ℕ → NNReal) : (Φ.extend fun (n : ℕ) => ↑(a n)) = ⨆ (N : ℕ), ↑(Φ (Finsupp.indicator (Finset.range N) fun (n : ℕ) (x : n ∈ Finset.range N) => a n))

The truncation formula: on a finite-valued sequence, the extension is the supremum of the gauge along the initial truncations a^{<N} of the sequence.

@[simp]

theorem TauCeti.SymmetricGauge.extend_smul (Φ : SymmetricGauge) (c : ENNReal) (a : ℕ → ENNReal) : Φ.extend (c • a) = c * Φ.extend a

The extension is homogeneous: Φ∞(c a) = c Φ∞(a) for every c : ℝ≥0∞.

theorem TauCeti.SymmetricGauge.extend_add_le (Φ : SymmetricGauge) (a b : ℕ → ENNReal) : Φ.extend (a + b) ≤ Φ.extend a + Φ.extend b

The extension is subadditive: Φ∞(a + b) ≤ Φ∞(a) + Φ∞(b).

The supremum gauge

noncomputable def TauCeti.SymmetricGauge.supGauge : SymmetricGauge

The supremum ⨆ n, a n of a finitely supported sequence, as a symmetric gauge. It is the least symmetric gauge (TauCeti.SymmetricGauge.iSup_le_apply), and its extension is the supremum of an arbitrary sequence (TauCeti.SymmetricGauge.extend_supGauge).

@[simp]

theorem TauCeti.SymmetricGauge.supGauge_apply (a : ℕ →₀ NNReal) : supGauge a = ⨆ (n : ℕ), a n

@[simp]

theorem TauCeti.SymmetricGauge.extend_supGauge (a : ℕ → ENNReal) : supGauge.extend a = ⨆ (n : ℕ), a n

The extension of the supremum gauge is the supremum of the sequence.

Restriction to finitely many coordinates and weak majorization

noncomputable def TauCeti.SymmetricGauge.finSeminorm (Φ : SymmetricGauge) (n : ℕ) : Seminorm ℝ (Fin n → ℝ)

The restriction of a symmetric gauge to the first n coordinates, as a seminorm on real n-tuples: x ↦ Φ (|x 0|, …, |x (n - 1)|, 0, 0, …). It is a symmetric gauge on Fin n → ℝ (TauCeti.SymmetricGauge.isSymmetricGauge_finSeminorm).

@[simp]

theorem TauCeti.SymmetricGauge.finSeminorm_apply (Φ : SymmetricGauge) (n : ℕ) (x : Fin n → ℝ) : (Φ.finSeminorm n) x = ↑(Φ (Finsupp.indicator (Finset.range n) fun (k : ℕ) (hk : k ∈ Finset.range n) => ‖x ⟨k, ⋯⟩‖₊))

theorem TauCeti.SymmetricGauge.isSymmetricGauge_finSeminorm (Φ : SymmetricGauge) (n : ℕ) : (Φ.finSeminorm n).IsSymmetricGauge

The restriction of a symmetric gauge to the first n coordinates is a symmetric gauge on real n-tuples.

theorem TauCeti.SymmetricGauge.apply_le_apply_of_forall_sum_le (Φ : SymmetricGauge) {a b : ℕ →₀ NNReal} (ha : Antitone ⇑a) (h : ∀ (k : ℕ), ∑ n ∈ Finset.range k, a n ≤ ∑ n ∈ Finset.range k, b n) : Φ a ≤ Φ b

Symmetric gauges are monotone for weak majorization, finitely supported form: if a is antitone and every partial sum of a is at most the corresponding partial sum of b, then Φ a ≤ Φ b. No order condition is needed on b.

theorem TauCeti.SymmetricGauge.extend_le_extend_of_forall_sum_le (Φ : SymmetricGauge) {a b : ℕ → ENNReal} (ha : Antitone a) (h : ∀ (k : ℕ), ∑ n ∈ Finset.range k, a n ≤ ∑ n ∈ Finset.range k, b n) : Φ.extend a ≤ Φ.extend b

Symmetric gauges are monotone for weak majorization. If a is antitone and every partial sum of a is at most the corresponding partial sum of b, then Φ∞ a ≤ Φ∞ b. No order condition is needed on b, and the sequences may take the value ∞.