Hilbert–Schmidt operators as ℓ² families of columns

Fix a Hilbert basis (bᵢ) of E. A family of vectors f ∈ ℓ²(ι, F) represents the bounded operator

T_f x = ∑' i, ⟪bᵢ, x⟫ • fᵢ,

whose columns are T_f bᵢ = fᵢ. This file shows that f ↦ T_f is a bounded linear injection ℓ²(ι, F) →L[𝕜] (E →L[𝕜] F) of norm at most 1, whose image is exactly the set of operators of finite Hilbert–Schmidt energy E_b(T) = ∑' i, ‖T bᵢ‖ₑ²; the inverse sends such an operator to its column family i ↦ T bᵢ. The energy of T_f is ‖f‖², so the Hilbert–Schmidt norm of T_f is the ℓ² norm of f.

Each T_f is a norm limit of the finite-rank operators attached to the finitely supported truncations of f, so it is compact. Consequently every operator of finite Hilbert–Schmidt energy is compact.

Main definitions

• HilbertBasis.columnOperator b : ℓ²(ι, F) →L[𝕜] E →L[𝕜] F: the operator T_f represented by an ℓ² family of columns f, relative to the Hilbert basis b.

Main results

• HilbertBasis.columnOperator_apply_self: the columns of T_f are f, T_f bᵢ = fᵢ.
• HilbertBasis.columnOperator_injective: distinct column families give distinct operators.
• HilbertBasis.columnOperator_eq_iff: T_f = T exactly when fᵢ = T bᵢ for every i.
• HilbertBasis.columnOperator_mk: an operator whose columns are square-summable is the operator represented by its columns.
• HilbertBasis.range_columnOperator: the represented operators are exactly the operators of finite Hilbert–Schmidt energy, and HilbertBasis.existsUnique_columnOperator_eq gives the unique representative.
• HilbertBasis.norm_columnOperator_apply_le, HilbertBasis.norm_columnOperator_le: ‖T_f‖ ≤ ‖f‖.
• HilbertBasis.hilbertSchmidtEnergy_columnOperator and HilbertBasis.hilbertSchmidtNorm_columnOperator: E_b(T_f) = ‖f‖ₑ² and ‖T_f‖_HS = ‖f‖.
• ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_memℓp and ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_summable: an operator has finite energy exactly when its columns lie in ℓ².
• ContinuousLinearMap.isCompactOperator_of_hilbertSchmidtEnergy_ne_top: Hilbert–Schmidt operators are compact.

References

• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised edition, Academic Press, 1980, Section VI.6.
• B. Simon, Trace Ideals and Their Applications, second edition, Mathematical Surveys and Monographs 120, American Mathematical Society, 2005, Section 2.

theorem HilbertBasis.summable_norm_inner_mul_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : Summable fun (i : ι) => ‖inner 𝕜 (b i) x‖ * ‖↑f i‖

The series ∑' i, ⟪bᵢ, x⟫ • fᵢ defining the operator represented by f ∈ ℓ²(ι, F) converges absolutely: by Cauchy–Schwarz in ℓ², ∑' i, ‖⟪bᵢ, x⟫‖ ‖fᵢ‖ ≤ ‖x‖ ‖f‖.

theorem HilbertBasis.tsum_norm_inner_mul_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : ∑' (i : ι), ‖inner 𝕜 (b i) x‖ * ‖↑f i‖ ≤ ‖x‖ * ‖f‖

Cauchy–Schwarz for the column series. ∑' i, ‖⟪bᵢ, x⟫‖ ‖fᵢ‖ ≤ ‖x‖ ‖f‖.

theorem HilbertBasis.norm_tsum_inner_smul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : ‖∑' (i : ι), inner 𝕜 (b i) x • ↑f i‖ ≤ ‖f‖ * ‖x‖

The column series is bounded by ‖f‖ ‖x‖.

theorem HilbertBasis.summable_inner_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : Summable fun (i : ι) => inner 𝕜 (b i) x • ↑f i

The column series ∑' i, ⟪bᵢ, x⟫ • fᵢ converges in a complete target.

noncomputable def HilbertBasis.columnOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] : ↥(lp (fun (x : ι) => F) 2) →L[𝕜] E →L[𝕜] F

The operator represented by an ℓ² family of columns: relative to a Hilbert basis (bᵢ) of E, the family f ∈ ℓ²(ι, F) represents x ↦ ∑' i, ⟪bᵢ, x⟫ • fᵢ, whose columns are fᵢ (columnOperator_apply_self). The assignment f ↦ T_f is linear and bounded with norm at most 1.

theorem HilbertBasis.columnOperator_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : (b.columnOperator f) x = ∑' (i : ι), inner 𝕜 (b i) x • ↑f i

theorem HilbertBasis.hasSum_columnOperator_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) (x : E) : HasSum (fun (i : ι) => inner 𝕜 (b i) x • ↑f i) ((b.columnOperator f) x)

The column series sums to the value of the represented operator.

@[simp]

theorem HilbertBasis.columnOperator_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) (i : ι) : (b.columnOperator f) (b i) = ↑f i

The columns of the represented operator. T_f bᵢ = fᵢ.

theorem HilbertBasis.columnOperator_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] : Function.Injective ⇑b.columnOperator

Injectivity of the column representation. An operator determines the ℓ² family of columns representing it.

theorem HilbertBasis.columnOperator_eq_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] {f : ↥(lp (fun (x : ι) => F) 2)} {T : E →L[𝕜] F} : b.columnOperator f = T ↔ ∀ (i : ι), ↑f i = T (b i)

An ℓ² family represents the operator T exactly when it is the column family of T.

theorem HilbertBasis.columnOperator_mk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : Memℓp (fun (i : ι) => T (b i)) 2) : b.columnOperator ⟨fun (i : ι) => T (b i), hT⟩ = T

Reconstruction from columns. An operator whose columns i ↦ T bᵢ are square-summable is the operator represented by its columns.

theorem HilbertBasis.norm_columnOperator_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) : ‖b.columnOperator f‖ ≤ ‖f‖

Operator-norm bound. ‖T_f‖ ≤ ‖f‖.

theorem HilbertBasis.norm_columnOperator_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] : ‖b.columnOperator‖ ≤ 1

The column representation f ↦ T_f has norm at most 1.

theorem HilbertBasis.tsum_norm_columnOperator_apply_self_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) : ∑' (i : ι), ‖(b.columnOperator f) (b i)‖ ^ 2 = ‖f‖ ^ 2

The squared columns of T_f sum to ‖f‖².

theorem HilbertBasis.columnOperator_single {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] [DecidableEq ι] (i : ι) (v : F) : b.columnOperator (lp.single 2 i v) = ((innerSL 𝕜) (b i)).smulRight v

The family supported at one index represents a rank-one operator.

theorem HilbertBasis.isCompactOperator_columnOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) [NormedSpace 𝕜 F] [CompleteSpace F] (f : ↥(lp (fun (x : ι) => F) 2)) : IsCompactOperator ⇑(b.columnOperator f)

The represented operators are compact: T_f is the norm limit of the finite-rank operators represented by the finitely supported truncations of f.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b ≠ ⊤ ↔ Summable fun (i : ι) => ‖T (b i)‖ ^ 2

An operator has finite Hilbert–Schmidt energy exactly when its column family i ↦ T bᵢ is square-summable.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_memℓp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b ≠ ⊤ ↔ Memℓp (fun (i : ι) => T (b i)) 2

An operator has finite Hilbert–Schmidt energy exactly when its column family i ↦ T bᵢ lies in ℓ².

@[simp]

theorem HilbertBasis.hilbertSchmidtEnergy_columnOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (b : HilbertBasis ι 𝕜 E) (f : ↥(lp (fun (x : ι) => F) 2)) : (b.columnOperator f).hilbertSchmidtEnergy b = ‖f‖ₑ ^ 2

Energy identity. The Hilbert–Schmidt energy of T_f is ‖f‖ₑ².

theorem HilbertBasis.range_columnOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (b : HilbertBasis ι 𝕜 E) : Set.range ⇑b.columnOperator = {T : E →L[𝕜] F | T.hilbertSchmidtEnergy b ≠ ⊤}

The operators represented by ℓ² families of columns are exactly the operators of finite Hilbert–Schmidt energy.

theorem HilbertBasis.existsUnique_columnOperator_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (b : HilbertBasis ι 𝕜 E) {T : E →L[𝕜] F} (hT : T.hilbertSchmidtEnergy b ≠ ⊤) : ∃! f : ↥(lp (fun (x : ι) => F) 2), b.columnOperator f = T

Unique column representative. An operator of finite Hilbert–Schmidt energy is represented by exactly one ℓ² family of columns.

@[simp]

theorem HilbertBasis.hilbertSchmidtNorm_columnOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (b : HilbertBasis ι 𝕜 E) [CompleteSpace E] (f : ↥(lp (fun (x : ι) => F) 2)) : (b.columnOperator f).hilbertSchmidtNorm = ‖f‖

Hilbert–Schmidt norm identity. The Hilbert–Schmidt norm of T_f is the ℓ² norm of f.

theorem ContinuousLinearMap.isCompactOperator_of_hilbertSchmidtEnergy_ne_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {b : HilbertBasis ι 𝕜 E} {T : E →L[𝕜] F} (hT : T.hilbertSchmidtEnergy b ≠ ⊤) : IsCompactOperator ⇑T

Hilbert–Schmidt operators are compact. An operator of finite Hilbert–Schmidt energy is a compact operator.