Hilbert–Schmidt operators

DefinitionSquared Hilbert–Schmidt norm in a family#✓fully proved

Let \(H\) be a real inner product space, let \(T : H \to H\) be a continuous linear operator and let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\). The squared Hilbert–Schmidt norm of \(T\) in the family \((u_n)\) is the extended nonnegative real \(\sum_{n=0}^{\infty} \|T u_n\|^2\), the sum being taken in \([0, \infty]\). It is \(\infty\) exactly when the real series \(\sum_n \|T u_n\|^2\) diverges.

noncomputable def hsNormSq
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (T : H →L[ℝ] H) (u : ℕ → H) : ℝ≥0∞ :=
  ∑' n : ℕ, ENNReal.ofReal (‖T (u n)‖ ^ 2)

Used by 4

Used byCanonical Hilbert–Schmidt norm equals the matrix norm · Canonical Hilbert–Schmidt norm of the constructed operator · Extended Hilbert–Schmidt norm in a family · Squared Hilbert–Schmidt norm of the Green's operator

DefinitionExtended Hilbert–Schmidt norm in a family#✓fully proved

Let \(H\) be a real inner product space, let \(T : H \to H\) be a continuous linear operator and let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\). The Hilbert–Schmidt norm of \(T\) in the family \((u_n)\) is the square root, taken in \([0, \infty]\) with \(\sqrt{\infty} = \infty\), of the squared Hilbert–Schmidt norm \(\sum_{n=0}^{\infty} \|T u_n\|^2 \in [0, \infty]\).

In particular it is \(\infty\), not \(0\), when the series \(\sum_n \|T u_n\|^2\) diverges, for example for the identity operator when \((u_n)\) is an orthonormal basis of \(H\) indexed by \(\mathbb{N}\).

noncomputable def hsENNNorm
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (T : H →L[ℝ] H) (u : ℕ → H) : ℝ≥0∞ :=
  hsNormSq T u ^ (1 / 2 : ℝ)

Uses 1 · Used by 2

Statement usesSquared Hilbert–Schmidt norm in a family

Used byThe Hilbert–Schmidt norm of a finite-rank operator is controlled by its operator norm · The Hilbert–Schmidt norm bounds an operator on unit vectors

TheoremSquared ℓ² norm as a sum of squared coordinates#✓fully proved

Norm squared of an ℓ²(ℕ, 𝕜) vector is the sum of the squared coordinate norms.

theorem norm_sq_lp_eq_tsum (f : ℓ²(ℕ, 𝕜)) :
    ‖f‖ ^ 2 = ∑' i, ‖f i‖ ^ 2

Used by 9

Used byCanonical Hilbert–Schmidt norm equals the matrix norm · Hilbert–Schmidt norm of a rank-one matrix · Hilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Norm bound for the Hilbert–Schmidt linear map · Norm bound for the Schur linear map · Bound on the double weighted series in Schur's test · Weighted partial sums grouped by the first index · Partial sums of the weighted row series in Schur's test · Summability of the double weighted series in Schur's test

TheoremSquare-summability of coordinates of an ℓ² vector#✓fully proved

Summability of squared coordinate norms from Memℓp.

theorem summable_norm_sq_of_memℓp {f : ℕ → 𝕜} (hf : Memℓp f 2) :
    Summable fun i => ‖f i‖ ^ 2

Used by 9

Used byCanonical Hilbert–Schmidt norm equals the matrix norm · Hilbert–Schmidt norm of a rank-one matrix · Entries of a rank-one matrix are square-summable · Square-summability of a Hilbert–Schmidt image · Bound on the double weighted series in Schur's test · Weighted partial sums grouped by the first index · Partial sums of the weighted row series in Schur's test · Summability of the weighted row series in Schur's test · Summability of the double weighted series in Schur's test

TheoremSquare-summable sequences lie in ℓ²#✓fully proved

Memℓp at 2 from summability of squared norms.

theorem memℓp_of_summable_norm_sq {f : ℕ → 𝕜} (hf : Summable fun i => ‖f i‖ ^ 2) :
    Memℓp f 2

Used by 3

Used byRow vector of a Hilbert–Schmidt matrix · Hilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Coordinates of a Schur image lie in \(\ell^2\)

DefinitionHilbert–Schmidt matrix#✓fully proved

A matrix is Hilbert–Schmidt if the squared norms of its entries are summable.

def IsHilbertSchmidt (a : ℕ → ℕ → 𝕜) : Prop :=
  Summable fun p : ℕ × ℕ => ‖a p.1 p.2‖ ^ 2

Used by 38

Used byAdjoint of a Hilbert–Schmidt operator · Canonical Hilbert–Schmidt norm equals the matrix norm · Canonical Hilbert–Schmidt norm of the constructed operator · Operator with Hilbert–Schmidt matrix is the operator of its matrix · Hilbert–Schmidt coordinates as inner products with rows · Hilbert–Schmidt operator as a linear map · Pointwise action of the Hilbert–Schmidt linear map · Matrix of the Hilbert–Schmidt operator of a matrix · Squared Hilbert–Schmidt norm of a matrix · Hilbert–Schmidt norm of the truncation error as a tail sum · Hilbert–Schmidt operator on ℓ² · Additivity of the Hilbert–Schmidt operator · Pointwise action of the Hilbert–Schmidt operator · Hilbert–Schmidt operator is independent of the summability proof · Hilbert–Schmidt operator of a scalar multiple of a matrix · Hilbert–Schmidt operator of a difference of matrices · Row vector of a Hilbert–Schmidt matrix · Hilbert–Schmidt operators on \(\ell^2\) are compact · Bounded operator with Hilbert–Schmidt matrix is compact · Sum of Hilbert–Schmidt matrices is Hilbert–Schmidt · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt · Rank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt · Truncated matrices are Hilbert–Schmidt · Negation preserves the Hilbert–Schmidt property · Scalar multiple of a Hilbert–Schmidt matrix is Hilbert–Schmidt · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt · Conjugate transpose of a Hilbert–Schmidt matrix is Hilbert–Schmidt · Zero matrix is Hilbert–Schmidt · Hilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Norm bound for the Hilbert–Schmidt linear map · Operator norm is at most the Hilbert–Schmidt norm · Operator norm bounded by the Hilbert–Schmidt norm · Summability of the Hilbert–Schmidt coordinate series · Square-summability of a Hilbert–Schmidt image · Rows of a Hilbert–Schmidt matrix are square-summable · Hilbert–Schmidt norm of the truncation error tends to zero · Truncated operators converge in norm to the Hilbert–Schmidt operator · Square partial sums converge to the squared Hilbert–Schmidt norm

DefinitionSquared Hilbert–Schmidt norm of a matrix#✓fully proved

The finite squared Hilbert–Schmidt norm: the sum of the squared entry norms. The witness restricts this real quantity to summable matrices, avoiding the zero default of a nonsummable real tsum. Divergent operators are handled by the existing extended-valued operator norm.

noncomputable def hsNormSq (a : ℕ → ℕ → 𝕜) (_ha : IsHilbertSchmidt a) : ℝ :=
  ∑' p : ℕ × ℕ, ‖a p.1 p.2‖ ^ 2

Uses 1 · Used by 12

Statement usesHilbert–Schmidt matrix

Used byCanonical Hilbert–Schmidt norm equals the matrix norm · Canonical Hilbert–Schmidt norm of the constructed operator · Hilbert–Schmidt norm of a diagonal matrix · Hilbert–Schmidt norm of a rank-one matrix · Hilbert–Schmidt norm of the truncation error as a tail sum · Hilbert–Schmidt operator on ℓ² · Norm bound for the Hilbert–Schmidt linear map · Operator norm is at most the Hilbert–Schmidt norm · Operator norm bounded by the Hilbert–Schmidt norm · Hilbert–Schmidt norm of the truncation error tends to zero · Truncated operators converge in norm to the Hilbert–Schmidt operator · Square partial sums converge to the squared Hilbert–Schmidt norm

TheoremRows of a Hilbert–Schmidt matrix are square-summable#✓fully proved

Fiber summability: each row of a Hilbert–Schmidt matrix is square-summable.

theorem summable_row_of_isHilbertSchmidt {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (i : ℕ) :
    Summable fun j => ‖a i j‖ ^ 2

Uses 1 · Used by 2

Statement usesHilbert–Schmidt matrix

Used byRow vector of a Hilbert–Schmidt matrix · Norm bound for the Hilbert–Schmidt linear map

DefinitionRow vector of a Hilbert–Schmidt matrix#✓fully proved

The row vector of a Hilbert–Schmidt matrix, as an ℓ² element (conjugated).

noncomputable def hsRow (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (i : ℕ) : ℓ²(ℕ, 𝕜) :=
  ⟨fun j => star (a i j), by
    apply memℓp_of_summable_norm_sq
    simpa [norm_star] using summable_row_of_isHilbertSchmidt ha i⟩

Uses 3 · Used by 4

Statement usesHilbert–Schmidt matrix · Square-summable sequences lie in ℓ² · Rows of a Hilbert–Schmidt matrix are square-summable

Used byHilbert–Schmidt coordinates as inner products with rows · Hilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Norm bound for the Hilbert–Schmidt linear map · Summability of the Hilbert–Schmidt coordinate series

TheoremSummability of the Hilbert–Schmidt coordinate series#✓fully proved

The coordinate series defining the Hilbert–Schmidt operator is summable.

theorem summable_hsCoord {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    Summable fun j => a i j * x j

Uses 2 · Used by 3

Statement usesHilbert–Schmidt matrix

Proof usesRow vector of a Hilbert–Schmidt matrix

Used byHilbert–Schmidt operator as a linear map · Additivity of the Hilbert–Schmidt operator · Hilbert–Schmidt operator of a difference of matrices

TheoremHilbert–Schmidt coordinates as inner products with rows#✓fully proved

The coordinate series is the inner product with the row vector.

theorem hsCoord_eq_inner {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (∑' j, a i j * x j) = ⟪hsRow a ha i, x⟫_𝕜

Uses 2 · Used by 2

Statement usesHilbert–Schmidt matrix · Row vector of a Hilbert–Schmidt matrix

Used byHilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Norm bound for the Hilbert–Schmidt linear map

TheoremHilbert–Schmidt matrix maps ℓ² vectors into ℓ²#✓fully proved

The coordinate series of a Hilbert–Schmidt matrix applied to an ℓ² vector is in ℓ².

theorem memℓp_hsCoord {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) :
    Memℓp (fun i => ∑' j, a i j * x j) 2

Uses 5 · Used by 2

Statement usesHilbert–Schmidt matrix

Proof usesHilbert–Schmidt coordinates as inner products with rows · Row vector of a Hilbert–Schmidt matrix · Square-summable sequences lie in ℓ² · Squared ℓ² norm as a sum of squared coordinates

Used byHilbert–Schmidt operator as a linear map · Square-summability of a Hilbert–Schmidt image

DefinitionHilbert–Schmidt operator as a linear map#✓fully proved

The Hilbert–Schmidt operator of a matrix, as a linear map.

MathlibExt.Analysis.InnerProductSpace.HilbertSchmidt.hsLinMap · 17 lines

noncomputable def hsLinMap (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨fun i => ∑' j, a i j * x j, memℓp_hsCoord ha x⟩
  map_add' x y := by
    apply lp.ext
    funext i
    show (∑' j, a i j * (x + y) j) = (∑' j, a i j * x j) + (∑' j, a i j * y j)
    rw [← (summable_hsCoord ha x i).tsum_add (summable_hsCoord ha y i)]
    refine tsum_congr (fun j => ?_)
    simp only [lp.coeFn_add, Pi.add_apply, mul_add]
  map_smul' c x := by
    apply lp.ext
    funext i
    show (∑' j, a i j * (c • x) j) = c * (∑' j, a i j * x j)
    rw [← tsum_mul_left]
    refine tsum_congr (fun j => ?_)
    rw [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, mul_left_comm]

Uses 3 · Used by 4

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Summability of the Hilbert–Schmidt coordinate series

Used byPointwise action of the Hilbert–Schmidt linear map · Hilbert–Schmidt operator on ℓ² · Norm bound for the Hilbert–Schmidt linear map · Square-summability of a Hilbert–Schmidt image

TheoremSquare-summability of a Hilbert–Schmidt image#✓fully proved

The squared norms of the coordinates of a Hilbert–Schmidt image are summable.

theorem summable_norm_sq_hsLinMap (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) :
    Summable fun i => ‖hsLinMap a ha x i‖ ^ 2

Uses 4 · Used by 1

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator as a linear map

Proof usesHilbert–Schmidt matrix maps ℓ² vectors into ℓ² · Square-summability of coordinates of an ℓ² vector

Used byNorm bound for the Hilbert–Schmidt linear map

TheoremPointwise action of the Hilbert–Schmidt linear map#✓fully proved

Pointwise action of the Hilbert–Schmidt linear map.

theorem hsLinMap_apply (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hsLinMap a ha x i = ∑' j, a i j * x j

Uses 2

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator as a linear map

TheoremNorm bound for the Hilbert–Schmidt linear map#✓fully proved

The Hilbert–Schmidt operator is bounded by the square root of hsNormSq.

theorem norm_hsLinMap_le (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) :
    ‖hsLinMap a ha x‖ ≤ Real.sqrt (hsNormSq a ha) * ‖x‖

Uses 8 · Used by 2

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator as a linear map · Squared Hilbert–Schmidt norm of a matrix

Proof usesHilbert–Schmidt coordinates as inner products with rows · Row vector of a Hilbert–Schmidt matrix · Squared ℓ² norm as a sum of squared coordinates · Square-summability of a Hilbert–Schmidt image · Rows of a Hilbert–Schmidt matrix are square-summable

Used byHilbert–Schmidt operator on ℓ² · Operator norm is at most the Hilbert–Schmidt norm

DefinitionHilbert–Schmidt operator on ℓ²#✓fully proved

The Hilbert–Schmidt operator of a matrix, as a bounded operator on ℓ²(ℕ, 𝕜).

noncomputable def hsOperator (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  (hsLinMap a ha).mkContinuous (Real.sqrt (hsNormSq a ha)) (norm_hsLinMap_le a ha)

Uses 4 · Used by 19

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator as a linear map · Squared Hilbert–Schmidt norm of a matrix · Norm bound for the Hilbert–Schmidt linear map

Used byAdjoint of a Hilbert–Schmidt operator · Canonical Hilbert–Schmidt norm of the constructed operator · Operator with Hilbert–Schmidt matrix is the operator of its matrix · Matrix of the Hilbert–Schmidt operator of a matrix · Additivity of the Hilbert–Schmidt operator · Pointwise action of the Hilbert–Schmidt operator · Hilbert–Schmidt operator is independent of the summability proof · Diagonal Hilbert–Schmidt operator acts by pointwise multiplication · Action of a rank-one Hilbert–Schmidt operator · Truncated Hilbert–Schmidt operator as a sum of rank-one operators · Hilbert–Schmidt operator of a scalar multiple of a matrix · Hilbert–Schmidt operator of a difference of matrices · Hilbert–Schmidt operator of the zero matrix is zero · Hilbert–Schmidt operators on \(\ell^2\) are compact · Truncated Hilbert–Schmidt operators are compact · Bounded operator with Hilbert–Schmidt matrix is compact · Operator norm is at most the Hilbert–Schmidt norm · Operator norm bounded by the Hilbert–Schmidt norm · Truncated operators converge in norm to the Hilbert–Schmidt operator

TheoremPointwise action of the Hilbert–Schmidt operator#✓fully proved

Pointwise action of the Hilbert–Schmidt operator.

theorem hsOperator_apply (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hsOperator a ha x i = ∑' j, a i j * x j

Uses 2 · Used by 5

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ²

Used byOperator with Hilbert–Schmidt matrix is the operator of its matrix · Matrix of the Hilbert–Schmidt operator of a matrix · Diagonal Hilbert–Schmidt operator acts by pointwise multiplication · Action of a rank-one Hilbert–Schmidt operator · Truncated Hilbert–Schmidt operator as a sum of rank-one operators

TheoremOperator norm is at most the Hilbert–Schmidt norm#✓fully proved

The operator norm of a Hilbert–Schmidt operator is at most its Hilbert–Schmidt norm.

theorem norm_hsOperator_le (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    ‖hsOperator a ha‖ ≤ Real.sqrt (hsNormSq a ha)

Uses 4 · Used by 2

Statement usesHilbert–Schmidt matrix · Squared Hilbert–Schmidt norm of a matrix · Hilbert–Schmidt operator on ℓ²

Proof usesNorm bound for the Hilbert–Schmidt linear map

Used byOperator norm bounded by the Hilbert–Schmidt norm · Truncated operators converge in norm to the Hilbert–Schmidt operator

TheoremZero matrix is Hilbert–Schmidt#✓fully proved

The zero matrix is Hilbert–Schmidt.

theorem isHilbertSchmidt_zero : IsHilbertSchmidt (0 : ℕ → ℕ → 𝕜)

Uses 1 · Used by 1

Statement usesHilbert–Schmidt matrix

Used byHilbert–Schmidt operator of the zero matrix is zero

TheoremHilbert–Schmidt operator of the zero matrix is zero#✓fully proved

The Hilbert–Schmidt operator of the zero matrix is zero.

theorem hsOperator_zero : hsOperator (0 : ℕ → ℕ → 𝕜) isHilbertSchmidt_zero = 0

Uses 2

Statement usesHilbert–Schmidt operator on ℓ² · Zero matrix is Hilbert–Schmidt

TheoremNegation preserves the Hilbert–Schmidt property#✓fully proved

The negative of a Hilbert–Schmidt matrix is Hilbert–Schmidt.

theorem isHilbertSchmidt_neg {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) :
    IsHilbertSchmidt (-a)

Uses 1 · Used by 1

Statement usesHilbert–Schmidt matrix

Used byDifference of Hilbert–Schmidt matrices is Hilbert–Schmidt

TheoremSum of Hilbert–Schmidt matrices is Hilbert–Schmidt#✓fully proved

The sum of Hilbert–Schmidt matrices is Hilbert–Schmidt.

theorem isHilbertSchmidt_add {a b : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a)
    (hb : IsHilbertSchmidt b) : IsHilbertSchmidt (a + b)

Uses 1 · Used by 2

Statement usesHilbert–Schmidt matrix

Used byAdditivity of the Hilbert–Schmidt operator · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt

TheoremDifference of Hilbert–Schmidt matrices is Hilbert–Schmidt#✓fully proved

The difference of Hilbert–Schmidt matrices is Hilbert–Schmidt.

theorem isHilbertSchmidt_sub {a b : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a)
    (hb : IsHilbertSchmidt b) : IsHilbertSchmidt (a - b)

Uses 3 · Used by 4

Statement usesHilbert–Schmidt matrix

Proof usesSum of Hilbert–Schmidt matrices is Hilbert–Schmidt · Negation preserves the Hilbert–Schmidt property

Used byHilbert–Schmidt norm of the truncation error as a tail sum · Hilbert–Schmidt operator of a difference of matrices · Hilbert–Schmidt norm of the truncation error tends to zero · Truncated operators converge in norm to the Hilbert–Schmidt operator

TheoremScalar multiple of a Hilbert–Schmidt matrix is Hilbert–Schmidt#✓fully proved

A scalar multiple of a Hilbert–Schmidt matrix is Hilbert–Schmidt.

theorem isHilbertSchmidt_smul {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (c : 𝕜) :
    IsHilbertSchmidt (c • a)

Uses 1 · Used by 1

Statement usesHilbert–Schmidt matrix

Used byHilbert–Schmidt operator of a scalar multiple of a matrix

TheoremAdditivity of the Hilbert–Schmidt operator#✓fully proved

The Hilbert–Schmidt operator of a sum is the sum of the operators.

theorem hsOperator_add {a b : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (hb : IsHilbertSchmidt b) :
    hsOperator (a + b) (isHilbertSchmidt_add ha hb) = hsOperator a ha + hsOperator b hb

Uses 4

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ² · Sum of Hilbert–Schmidt matrices is Hilbert–Schmidt

Proof usesSummability of the Hilbert–Schmidt coordinate series

TheoremHilbert–Schmidt operator of a difference of matrices#✓fully proved

The Hilbert–Schmidt operator of a difference is the difference of the operators.

theorem hsOperator_sub {a b : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (hb : IsHilbertSchmidt b) :
    hsOperator (a - b) (isHilbertSchmidt_sub ha hb) = hsOperator a ha - hsOperator b hb

Uses 4 · Used by 1

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ² · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt

Proof usesSummability of the Hilbert–Schmidt coordinate series

Used byTruncated operators converge in norm to the Hilbert–Schmidt operator

TheoremHilbert–Schmidt operator of a scalar multiple of a matrix#✓fully proved

The Hilbert–Schmidt operator of a scalar multiple is the scalar multiple of the operator.

theorem hsOperator_smul {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) (c : 𝕜) :
    hsOperator (c • a) (isHilbertSchmidt_smul ha c) = c • hsOperator a ha

Uses 3

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ² · Scalar multiple of a Hilbert–Schmidt matrix is Hilbert–Schmidt

DefinitionConjugate transpose of an infinite matrix#✓fully proved

The conjugate transpose of a matrix: (aᵀ*) i j = star (a j i).

def hsTransposeStar (a : ℕ → ℕ → 𝕜) : ℕ → ℕ → 𝕜 := fun i j => star (a j i)

Used by 2

Used byAdjoint of a Hilbert–Schmidt operator · Conjugate transpose of a Hilbert–Schmidt matrix is Hilbert–Schmidt

TheoremConjugate transpose of a Hilbert–Schmidt matrix is Hilbert–Schmidt#✓fully proved

The conjugate transpose of a Hilbert–Schmidt matrix is Hilbert–Schmidt.

theorem isHilbertSchmidt_transposeStar {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) :
    IsHilbertSchmidt (hsTransposeStar a)

Uses 2 · Used by 1

Statement usesHilbert–Schmidt matrix · Conjugate transpose of an infinite matrix

Used byAdjoint of a Hilbert–Schmidt operator

DefinitionMatrix of a bounded operator on \(\ell^2\)#✓fully proved

The matrix of a bounded operator on ℓ²(ℕ, 𝕜): entry (i, j) is the i-th coordinate of the image of the j-th standard basis vector.

def hsMatrix (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)) (i j : ℕ) : 𝕜 :=
  T (lp.single 2 j (1 : 𝕜)) i

Used by 7

Used byAdjoint of a Hilbert–Schmidt operator · Canonical Hilbert–Schmidt norm equals the matrix norm · Canonical Hilbert–Schmidt norm of the constructed operator · Operator with Hilbert–Schmidt matrix is the operator of its matrix · Matrix of the Hilbert–Schmidt operator of a matrix · Bounded operator with Hilbert–Schmidt matrix is compact · Operator norm bounded by the Hilbert–Schmidt norm

TheoremOperator with Hilbert–Schmidt matrix is the operator of its matrix#✓fully proved

A bounded operator whose matrix is Hilbert–Schmidt is the Hilbert–Schmidt operator of its matrix.

theorem eq_hsOperator_of_isHilbertSchmidt_matrix (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
    (hT : IsHilbertSchmidt (hsMatrix T)) :
    T = hsOperator (hsMatrix T) hT

Uses 4 · Used by 3

Statement usesHilbert–Schmidt matrix · Matrix of a bounded operator on \(\ell^2\) · Hilbert–Schmidt operator on ℓ²

Proof usesPointwise action of the Hilbert–Schmidt operator

Used byAdjoint of a Hilbert–Schmidt operator · Bounded operator with Hilbert–Schmidt matrix is compact · Operator norm bounded by the Hilbert–Schmidt norm

TheoremMatrix of the Hilbert–Schmidt operator of a matrix#✓fully proved

The matrix of a Hilbert–Schmidt operator is the matrix itself.

theorem hsMatrix_hsOperator (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    hsMatrix (hsOperator a ha) = a

Uses 4 · Used by 2

Statement usesHilbert–Schmidt matrix · Matrix of a bounded operator on \(\ell^2\) · Hilbert–Schmidt operator on ℓ²

Proof usesPointwise action of the Hilbert–Schmidt operator

Used byAdjoint of a Hilbert–Schmidt operator · Canonical Hilbert–Schmidt norm of the constructed operator

TheoremHilbert–Schmidt operator is independent of the summability proof#✓fully proved

The Hilbert–Schmidt operator depends only on the matrix, not on the summability proof.

theorem hsOperator_congr {m m' : ℕ → ℕ → 𝕜} (h : m = m') (hm : IsHilbertSchmidt m)
    (hm' : IsHilbertSchmidt m') :
    hsOperator m hm = hsOperator m' hm'

Uses 2 · Used by 1

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ²

Used byAdjoint of a Hilbert–Schmidt operator

TheoremAdjoint of a Hilbert–Schmidt operator#✓fully proved

The adjoint of a Hilbert–Schmidt operator is the Hilbert–Schmidt operator of the conjugate-transpose matrix.

theorem adjoint_hsOperator (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    (hsOperator a ha)† =
      hsOperator (hsTransposeStar a) (isHilbertSchmidt_transposeStar ha)

Uses 8

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ² · Conjugate transpose of an infinite matrix · Conjugate transpose of a Hilbert–Schmidt matrix is Hilbert–Schmidt

Proof usesOperator with Hilbert–Schmidt matrix is the operator of its matrix · Matrix of a bounded operator on \(\ell^2\) · Matrix of the Hilbert–Schmidt operator of a matrix · Hilbert–Schmidt operator is independent of the summability proof

DefinitionTruncation of a matrix to its top-left block#✓fully proved

The truncation of a matrix to the top-left N × N block.

def hsTrunc (a : ℕ → ℕ → 𝕜) (N : ℕ) : ℕ → ℕ → 𝕜 :=
  fun i j => if i < N ∧ j < N then a i j else 0

Used by 7

Used byHilbert–Schmidt norm of the truncation error as a tail sum · Truncated Hilbert–Schmidt operator as a sum of rank-one operators · Hilbert–Schmidt operators on \(\ell^2\) are compact · Truncated Hilbert–Schmidt operators are compact · Truncated matrices are Hilbert–Schmidt · Hilbert–Schmidt norm of the truncation error tends to zero · Truncated operators converge in norm to the Hilbert–Schmidt operator

TheoremTruncated matrices are Hilbert–Schmidt#✓fully proved

A truncation of any matrix is Hilbert–Schmidt: it is supported on a finite set.

theorem isHilbertSchmidt_hsTrunc (a : ℕ → ℕ → 𝕜) (N : ℕ) :
    IsHilbertSchmidt (hsTrunc a N)

Uses 2 · Used by 6

Statement usesHilbert–Schmidt matrix · Truncation of a matrix to its top-left block

Used byHilbert–Schmidt norm of the truncation error as a tail sum · Truncated Hilbert–Schmidt operator as a sum of rank-one operators · Hilbert–Schmidt operators on \(\ell^2\) are compact · Truncated Hilbert–Schmidt operators are compact · Hilbert–Schmidt norm of the truncation error tends to zero · Truncated operators converge in norm to the Hilbert–Schmidt operator

TheoremRank-one operators on \(\ell^2\) are compact#✓fully proved

A rank-one operator on ℓ² is compact: it factors through the one-dimensional space 𝕜.

theorem isCompactOperator_rankOne (x y : ℓ²(ℕ, 𝕜)) :
    IsCompactOperator (InnerProductSpace.rankOne 𝕜 x y)

Used by 1

Used byTruncated Hilbert–Schmidt operators are compact

TheoremScaled rank-one operator on standard basis vectors#✓fully proved

The action of a scaled rank-one operator on standard basis vectors, pointwise.

theorem rankOne_single_apply (b : 𝕜) (i j : ℕ) (x : ℓ²(ℕ, 𝕜)) (k : ℕ) :
    ((b • InnerProductSpace.rankOne 𝕜 (lp.single (E := fun _ : ℕ => 𝕜) 2 i (1 : 𝕜))
      (lp.single (E := fun _ : ℕ => 𝕜) 2 j (1 : 𝕜))) x) k =
      if k = i then b * x j else 0

Used by 1

Used byTruncated Hilbert–Schmidt operator as a sum of rank-one operators

TheoremTruncated Hilbert–Schmidt operator as a sum of rank-one operators#✓fully proved

A truncated Hilbert–Schmidt operator is a finite sum of rank-one operators.

theorem hsOperator_hsTrunc_eq_sum (a : ℕ → ℕ → 𝕜) (N : ℕ) :
    hsOperator (hsTrunc a N) (isHilbertSchmidt_hsTrunc a N) =
      ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
        (a i j) • InnerProductSpace.rankOne 𝕜
          (lp.single (E := fun _ : ℕ => 𝕜) 2 i (1 : 𝕜))
          (lp.single (E := fun _ : ℕ => 𝕜) 2 j (1 : 𝕜))

Uses 5 · Used by 1

Statement usesHilbert–Schmidt operator on ℓ² · Truncation of a matrix to its top-left block · Truncated matrices are Hilbert–Schmidt

Proof usesPointwise action of the Hilbert–Schmidt operator · Scaled rank-one operator on standard basis vectors

Used byTruncated Hilbert–Schmidt operators are compact

TheoremTruncated Hilbert–Schmidt operators are compact#✓fully proved

A truncated Hilbert–Schmidt operator is compact.

theorem isCompactOperator_hsOperator_hsTrunc (a : ℕ → ℕ → 𝕜) (N : ℕ) :
    IsCompactOperator (hsOperator (hsTrunc a N) (isHilbertSchmidt_hsTrunc a N))

Uses 5 · Used by 1

Statement usesHilbert–Schmidt operator on ℓ² · Truncation of a matrix to its top-left block · Truncated matrices are Hilbert–Schmidt

Proof usesTruncated Hilbert–Schmidt operator as a sum of rank-one operators · Rank-one operators on \(\ell^2\) are compact

Used byHilbert–Schmidt operators on \(\ell^2\) are compact

TheoremHilbert–Schmidt norm of the truncation error as a tail sum#✓fully proved

The squared Hilbert–Schmidt norm of the truncation error is the tail sum.

theorem hsNormSq_sub_hsTrunc (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) (N : ℕ) :
    hsNormSq (a - hsTrunc a N)
      (isHilbertSchmidt_sub ha (isHilbertSchmidt_hsTrunc a N)) =
      hsNormSq a ha - ∑ p ∈ Finset.range N ×ˢ Finset.range N, ‖a p.1 p.2‖ ^ 2

Uses 5 · Used by 1

Statement usesHilbert–Schmidt matrix · Squared Hilbert–Schmidt norm of a matrix · Truncation of a matrix to its top-left block · Truncated matrices are Hilbert–Schmidt · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt

Used byHilbert–Schmidt norm of the truncation error tends to zero

TheoremSquare partial sums converge to the squared Hilbert–Schmidt norm#✓fully proved

The partial sums of the squared norms over expanding squares converge to hsNormSq.

theorem tendsto_hsTrunc_finset_sum {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) :
    Tendsto (fun N => ∑ p ∈ Finset.range N ×ˢ Finset.range N, ‖a p.1 p.2‖ ^ 2) atTop
      (𝓝 (hsNormSq a ha))

Uses 2 · Used by 1

Statement usesHilbert–Schmidt matrix · Squared Hilbert–Schmidt norm of a matrix

Used byHilbert–Schmidt norm of the truncation error tends to zero

TheoremHilbert–Schmidt norm of the truncation error tends to zero#✓fully proved

The squared Hilbert–Schmidt norm of the truncation error tends to zero.

theorem tendsto_hsNormSq_sub_hsTrunc {a : ℕ → ℕ → 𝕜} (ha : IsHilbertSchmidt a) :
    Tendsto (fun N => hsNormSq (a - hsTrunc a N)
      (isHilbertSchmidt_sub ha (isHilbertSchmidt_hsTrunc a N))) atTop (𝓝 0)

Uses 7 · Used by 1

Statement usesHilbert–Schmidt matrix · Squared Hilbert–Schmidt norm of a matrix · Truncation of a matrix to its top-left block · Truncated matrices are Hilbert–Schmidt · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt

Proof usesHilbert–Schmidt norm of the truncation error as a tail sum · Square partial sums converge to the squared Hilbert–Schmidt norm

Used byTruncated operators converge in norm to the Hilbert–Schmidt operator

TheoremTruncated operators converge in norm to the Hilbert–Schmidt operator#✓fully proved

The truncated operators converge in norm to the Hilbert–Schmidt operator.

theorem tendsto_hsOperator_hsTrunc (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    Tendsto (fun N => hsOperator (hsTrunc a N) (isHilbertSchmidt_hsTrunc a N)) atTop
      (𝓝 (hsOperator a ha))

Uses 9 · Used by 1

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ² · Truncation of a matrix to its top-left block · Truncated matrices are Hilbert–Schmidt

Proof usesSquared Hilbert–Schmidt norm of a matrix · Hilbert–Schmidt operator of a difference of matrices · Difference of Hilbert–Schmidt matrices is Hilbert–Schmidt · Operator norm is at most the Hilbert–Schmidt norm · Hilbert–Schmidt norm of the truncation error tends to zero

Used byHilbert–Schmidt operators on \(\ell^2\) are compact

TheoremHilbert–Schmidt operators on \(\ell^2\) are compact#✓fully proved

Every Hilbert–Schmidt operator on ℓ²(ℕ, 𝕜) is compact.

theorem isCompactOperator_hsOperator (a : ℕ → ℕ → 𝕜) (ha : IsHilbertSchmidt a) :
    IsCompactOperator (hsOperator a ha)

Uses 6 · Used by 1

Statement usesHilbert–Schmidt matrix · Hilbert–Schmidt operator on ℓ²

Proof usesTruncation of a matrix to its top-left block · Truncated Hilbert–Schmidt operators are compact · Truncated matrices are Hilbert–Schmidt · Truncated operators converge in norm to the Hilbert–Schmidt operator

Used byBounded operator with Hilbert–Schmidt matrix is compact

TheoremBounded operator with Hilbert–Schmidt matrix is compact#✓fully proved

A bounded operator whose matrix is Hilbert–Schmidt is compact.

theorem isCompactOperator_of_isHilbertSchmidt_matrix (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
    (hT : IsHilbertSchmidt (hsMatrix T)) : IsCompactOperator T

Uses 5

Statement usesHilbert–Schmidt matrix · Matrix of a bounded operator on \(\ell^2\)

Proof usesOperator with Hilbert–Schmidt matrix is the operator of its matrix · Hilbert–Schmidt operator on ℓ² · Hilbert–Schmidt operators on \(\ell^2\) are compact

TheoremOperator norm bounded by the Hilbert–Schmidt norm#✓fully proved

A bounded operator whose matrix is Hilbert–Schmidt has norm at most its Hilbert–Schmidt norm.

theorem norm_le_of_isHilbertSchmidt_matrix (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
    (hT : IsHilbertSchmidt (hsMatrix T)) :
    ‖T‖ ≤ Real.sqrt (hsNormSq (hsMatrix T) hT)

Uses 6

Statement usesHilbert–Schmidt matrix · Matrix of a bounded operator on \(\ell^2\) · Squared Hilbert–Schmidt norm of a matrix

Proof usesOperator with Hilbert–Schmidt matrix is the operator of its matrix · Hilbert–Schmidt operator on ℓ² · Operator norm is at most the Hilbert–Schmidt norm

DefinitionDiagonal infinite matrix#✓fully proved

The diagonal matrix with diagonal d.

def hsDiagonal (d : ℕ → 𝕜) : ℕ → ℕ → 𝕜 := fun i j => if i = j then d i else 0

Used by 5

Used byHilbert–Schmidt norm of a diagonal matrix · Diagonal Hilbert–Schmidt operator acts by pointwise multiplication · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt · Rows of a diagonal matrix are square-summable · Squared row norm of a diagonal matrix

TheoremRows of a diagonal matrix are square-summable#✓fully proved

A row of a diagonal matrix is square-summable.

theorem summable_hsDiagonal_row (d : ℕ → 𝕜) (i : ℕ) :
    Summable fun j => ‖hsDiagonal d i j‖ ^ 2

Uses 1 · Used by 2

Statement usesDiagonal infinite matrix

Used byHilbert–Schmidt norm of a diagonal matrix · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt

TheoremSquared row norm of a diagonal matrix#✓fully proved

The squared norms in a row of a diagonal matrix sum to the squared diagonal entry.

theorem tsum_hsDiagonal_row (d : ℕ → 𝕜) (i : ℕ) :
    ∑' j, ‖hsDiagonal d i j‖ ^ 2 = ‖d i‖ ^ 2

Uses 1 · Used by 2

Statement usesDiagonal infinite matrix

Used byHilbert–Schmidt norm of a diagonal matrix · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt

TheoremDiagonal matrix with square-summable diagonal is Hilbert–Schmidt#✓fully proved

A diagonal matrix with square-summable diagonal is Hilbert–Schmidt.

theorem isHilbertSchmidt_hsDiagonal {d : ℕ → 𝕜} (hd : Summable fun i => ‖d i‖ ^ 2) :
    IsHilbertSchmidt (hsDiagonal d)

Uses 4 · Used by 2

Statement usesHilbert–Schmidt matrix · Diagonal infinite matrix

Proof usesRows of a diagonal matrix are square-summable · Squared row norm of a diagonal matrix

Used byHilbert–Schmidt norm of a diagonal matrix · Diagonal Hilbert–Schmidt operator acts by pointwise multiplication

TheoremHilbert–Schmidt norm of a diagonal matrix#✓fully proved

The squared Hilbert–Schmidt norm of a diagonal matrix is the sum of the squared diagonal entries.

theorem hsNormSq_hsDiagonal {d : ℕ → 𝕜} (hd : Summable fun i => ‖d i‖ ^ 2) :
    hsNormSq (hsDiagonal d) (isHilbertSchmidt_hsDiagonal hd) = ∑' i, ‖d i‖ ^ 2

Uses 5

Statement usesDiagonal infinite matrix · Squared Hilbert–Schmidt norm of a matrix · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt

Proof usesRows of a diagonal matrix are square-summable · Squared row norm of a diagonal matrix

TheoremDiagonal Hilbert–Schmidt operator acts by pointwise multiplication#✓fully proved

A diagonal Hilbert–Schmidt operator acts by pointwise multiplication by the diagonal.

theorem hsOperator_hsDiagonal_apply {d : ℕ → 𝕜} (hd : Summable fun i => ‖d i‖ ^ 2)
    (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hsOperator (hsDiagonal d) (isHilbertSchmidt_hsDiagonal hd) x i = d i * x i

Uses 4

Statement usesDiagonal infinite matrix · Hilbert–Schmidt operator on ℓ² · Diagonal matrix with square-summable diagonal is Hilbert–Schmidt

Proof usesPointwise action of the Hilbert–Schmidt operator

DefinitionRank-one infinite matrix#✓fully proved

The rank-one matrix u i * star (v j).

def hsRankOne (u v : ℕ → 𝕜) : ℕ → ℕ → 𝕜 := fun i j => u i * star (v j)

Used by 3

Used byHilbert–Schmidt norm of a rank-one matrix · Action of a rank-one Hilbert–Schmidt operator · Rank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt

TheoremEntries of a rank-one matrix are square-summable#✓fully proved

The squared norms of the entries of a rank-one matrix are summable over the product.

theorem summable_hsRankOne_sq {u v : ℓ²(ℕ, 𝕜)} :
    Summable fun p : ℕ × ℕ => ‖u p.1‖ ^ 2 * ‖v p.2‖ ^ 2

Uses 1 · Used by 2

Proof usesSquare-summability of coordinates of an ℓ² vector

Used byHilbert–Schmidt norm of a rank-one matrix · Rank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt

TheoremRank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt#✓fully proved

A rank-one matrix with ℓ² vectors is Hilbert–Schmidt.

theorem isHilbertSchmidt_hsRankOne {u v : ℓ²(ℕ, 𝕜)} :
    IsHilbertSchmidt (hsRankOne u v)

Uses 3 · Used by 2

Statement usesHilbert–Schmidt matrix · Rank-one infinite matrix

Proof usesEntries of a rank-one matrix are square-summable

Used byHilbert–Schmidt norm of a rank-one matrix · Action of a rank-one Hilbert–Schmidt operator

TheoremAction of a rank-one Hilbert–Schmidt operator#✓fully proved

A rank-one Hilbert–Schmidt operator acts as the inner product with v times u.

theorem hsOperator_hsRankOne_apply {u v : ℓ²(ℕ, 𝕜)} (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hsOperator (hsRankOne u v) isHilbertSchmidt_hsRankOne x i =
      u i * ⟪v, x⟫_𝕜

Uses 4

Statement usesHilbert–Schmidt operator on ℓ² · Rank-one infinite matrix · Rank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt

Proof usesPointwise action of the Hilbert–Schmidt operator

TheoremHilbert–Schmidt norm of a rank-one matrix#✓fully proved

The squared Hilbert–Schmidt norm of a rank-one matrix is ‖u‖² * ‖v‖².

theorem hsNormSq_hsRankOne {u v : ℓ²(ℕ, 𝕜)} :
    hsNormSq (hsRankOne u v) isHilbertSchmidt_hsRankOne = ‖u‖ ^ 2 * ‖v‖ ^ 2

Uses 6

Statement usesSquared Hilbert–Schmidt norm of a matrix · Rank-one infinite matrix · Rank-one matrix of \(\ell^2\) vectors is Hilbert–Schmidt

Proof usesSquared ℓ² norm as a sum of squared coordinates · Entries of a rank-one matrix are square-summable · Square-summability of coordinates of an ℓ² vector

TheoremCanonical Hilbert–Schmidt norm equals the matrix norm#✓fully proved

In the standard ℓ² basis, the existing extended operator squared norm equals the finite matrix squared norm. This bridge is specialized to real scalars because the canonical operator norm API is real-only.

theorem canonical_hsNormSq_eq_ofReal_matrix (T : ℓ²(ℕ, ℝ) →L[ℝ] ℓ²(ℕ, ℝ))
    (hT : IsHilbertSchmidt (hsMatrix T)) :
    MathlibExt.Analysis.OperatorTheory.HilbertSchmidtNorm.hsNormSq T
      (fun j => lp.single 2 j (1 : ℝ)) = ENNReal.ofReal (hsNormSq (hsMatrix T) hT)

Uses 6 · Used by 1

Statement usesHilbert–Schmidt matrix · Matrix of a bounded operator on \(\ell^2\) · Squared Hilbert–Schmidt norm of a matrix · Squared Hilbert–Schmidt norm in a family

Proof usesSquared ℓ² norm as a sum of squared coordinates · Square-summability of coordinates of an ℓ² vector

Used byCanonical Hilbert–Schmidt norm of the constructed operator

TheoremCanonical Hilbert–Schmidt norm of the constructed operator#✓fully proved

The constructed real Hilbert–Schmidt operator has the canonical extended squared norm given by the finite squared norm of its matrix.

theorem canonical_hsNormSq_hsOperator (a : ℕ → ℕ → ℝ) (ha : IsHilbertSchmidt a) :
    MathlibExt.Analysis.OperatorTheory.HilbertSchmidtNorm.hsNormSq (hsOperator a ha)
      (fun j => lp.single 2 j (1 : ℝ)) = ENNReal.ofReal (hsNormSq a ha)

Uses 7

Statement usesHilbert–Schmidt matrix · Squared Hilbert–Schmidt norm of a matrix · Hilbert–Schmidt operator on ℓ² · Squared Hilbert–Schmidt norm in a family

Proof usesCanonical Hilbert–Schmidt norm equals the matrix norm · Matrix of a bounded operator on \(\ell^2\) · Matrix of the Hilbert–Schmidt operator of a matrix

TheoremThe Hilbert–Schmidt norm of a finite-rank operator is controlled by its operator norm#●ready to prove

There is a function \(C\) from the natural numbers to the positive reals with the following property. Let \(H\) be an infinite-dimensional separable real Hilbert space, let \((u_i)_{i \in \mathbb{N}}\) be a Hilbert basis of \(H\), and let \(T : H \to H\) be a bounded linear operator such that the quotient \(H/\ker T\) is finite-dimensional, of dimension \(n\). Then the Hilbert–Schmidt norm of \(T\) computed in the basis \((u_i)\), taken in \([0,\infty]\), satisfies

\[\Big(\sum_{i \in \mathbb{N}} \|Tu_i\|^2\Big)^{1/2} \le C(n)\,\|T\|,\]

where \(\|T\|\) is the operator norm of \(T\).

public theorem_wanted exists_hsNorm_le_mul_opNorm_of_finiteDimensional_quotient_ker :
    ∃ C : ℕ → ℝ, (∀ n : ℕ, 0 < C n) ∧
      ∀ (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
        [TopologicalSpace.SeparableSpace H] (hH : ¬ FiniteDimensional ℝ H)
        (T : H →L[ℝ] H) (b : HilbertBasis ℕ ℝ H)
        [FiniteDimensional ℝ (H ⧸ T.ker)],
        HilbertSchmidtNorm.hsENNNorm T (⇑b) ≤
          ENNReal.ofReal (C (Module.finrank ℝ (H ⧸ T.ker)) * ‖T‖)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_98.

Uses 1

Statement usesExtended Hilbert–Schmidt norm in a family

TheoremThe Hilbert–Schmidt norm bounds an operator on unit vectors#●ready to prove

Let \(H\) be a real Hilbert space, let \(T : H \to H\) be a bounded linear operator, and let \((u_n)_{n \in \mathbb{N}}\) be an orthonormal basis of \(H\) indexed by the natural numbers. Let \(\|T\|_{\mathrm{HS}} = \bigl(\sum_{n} \|T u_n\|^2\bigr)^{1/2} \in [0, \infty]\) be the Hilbert–Schmidt norm of \(T\) computed in this basis; it is \(\infty\) when the series diverges. Then \(\|Tx\| \le \|T\|_{\mathrm{HS}}\) for every \(x \in H\) with \(\|x\| = 1\).

public theorem_wanted norm_apply_le_hsNorm_of_norm_eq_one
    (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (T : H →L[ℝ] H)
    (u : HilbertBasis ℕ ℝ H) :
    ∀ x : H, ‖x‖ = 1 → ENNReal.ofReal ‖T x‖ ≤ HilbertSchmidtNorm.hsENNNorm T u

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Special classes of linear operators), problem ma_proofbench_l2_68.

Uses 1

Statement usesExtended Hilbert–Schmidt norm in a family

61 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.