The ℓᵖ symmetric gauges

For a finite real exponent p ≥ 1, the ℓᵖ norm on finitely supported nonnegative sequences is a symmetric gauge. Its extension to arbitrary nonnegative extended-real sequences is the p-th root of the sum of their p-th powers, including when the sum is infinite. Applied to approximation numbers, these gauges construct the Schatten operator ideals.

References

• B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapter 2.

noncomputable def TauCeti.SymmetricGauge.lpGauge (p : ℝ) (hp : 1 ≤ p) : SymmetricGauge

The ℓᵖ norm of a finitely supported nonnegative sequence, as a symmetric gauge.

@[simp]

theorem TauCeti.SymmetricGauge.lpGauge_apply (p : ℝ) (hp : 1 ≤ p) (a : ℕ →₀ NNReal) : (lpGauge p hp) a = (a.sum fun (x : ℕ) (x_1 : NNReal) => x_1 ^ p) ^ (1 / p)

The defining finite power-sum formula for the ℓᵖ gauge.

@[simp]

theorem TauCeti.SymmetricGauge.extend_lpGauge (p : ℝ) (hp : 1 ≤ p) (a : ℕ → ENNReal) : (lpGauge p hp).extend a = (∑' (n : ℕ), a n ^ p) ^ (1 / p)

The extension of the ℓᵖ gauge is the p-th root of the sum of the p-th powers. No finiteness or summability hypotheses are needed.