PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.Banach

The zero operator $0 : H \to H$ on a Hilbert space $H$ is trace-class.

Let $H$ be a complex Hilbert space and $T: H \to H$ be a continuous linear operator. For any complex scalar $c \in \mathbb{C}$, if $T$ is a trace-class operator, then the scalar multiple $c \cdot T$ is also a trace-class operator.

Let $H$ be a complex Hilbert space and $T: H \to H$ be a bounded linear operator. If $T$ is a trace-class operator, then its negation $-T$ is also a trace-class operator.

Let $H$ be a complex Hilbert space. The trace norm of the zero operator $0 : H \to H$ is equal to $0$, i.e., $\|0\|_1 = 0$.

Let $H$ be a complex Hilbert space and $T: H \to H$ be a continuous linear operator. For any complex scalar $c \in \mathbb{C}$, if $T$ is a trace-class operator, then the trace norm of the scalar multiple $c \cdot T$ is equal to the product of the absolute value of $c$ and the trace norm of $T$: $$\|c \cdot T\|_1 = |c| \|T\|_1$$ where $\|\cdot\|_1$ denotes the trace norm.

Let $H$ be a complex Hilbert space and let $T: H \to H$ be a continuous linear operator. If $T$ is a trace-class operator, then its negation $-T$ is also a trace-class operator, and the trace norm of $-T$ is equal to the trace norm of $T$, i.e., $\| -T \|_1 = \| T \|_1$.

For any trace-class operator $T$ on a complex Hilbert space $H$, the operator norm $\|T\|$ is less than or equal to the trace norm $\|T\|_1$.

Let $H$ be a complex Hilbert space and let $\mathcal{B}(H)$ (represented as `H →L[ℂ] H`) be the space of bounded linear operators on $H$. The `traceClassSubmodule` is the $\mathbb{C}$-submodule of $\mathcal{B}(H)$ consisting of all trace-class operators. It is defined by showing that the zero operator is trace-class, and that the property of being trace-class is preserved under operator addition and scalar multiplication by complex numbers $\mathbb{C}$.

Let $H$ be a complex Hilbert space. The trace-class Banach space $\mathcal{S}_1(H)$ is the space consisting of all trace-class bounded linear operators on $H$, equipped with the trace norm $\| \cdot \|_1$.

Let $H$ be a complex Hilbert space. The space of trace-class operators $\mathcal{S}_1(H)$ forms an additive abelian group under the standard addition of operators. This structure provides the definition for the sum of two trace-class operators, the zero operator, and the additive inverse (negation) of a trace-class operator within the space $\mathcal{S}_1(H)$.

Let $H$ be a complex Hilbert space. The space of trace-class operators $\mathcal{S}_1(H)$ forms a vector space (module) over the field of complex numbers $\mathbb{C}$. This structure defines the scalar multiplication of a trace-class operator by a complex number, such that for any $c \in \mathbb{C}$ and $T \in \mathcal{S}_1(H)$, the operator $cT$ is also an element of $\mathcal{S}_1(H)$.

Let $H$ be a complex Hilbert space and $T \in \mathcal{B}(H)$ be a bounded linear operator. $T$ belongs to the trace-class submodule of $\mathcal{B}(H)$ if and only if $T$ is a trace-class operator.

Let $H$ be a complex Hilbert space and let $\mathcal{S}_1(H)$ (denoted in the formal text as `TraceClass H`) be the Banach space of trace-class operators on $H$. For any element $T \in \mathcal{S}_1(H)$, the underlying bounded linear operator is a trace-class operator.

Given a bounded linear operator $T \in \mathcal{B}(H)$ on a complex Hilbert space $H$ and a proof $h_T$ that $T$ is trace-class (i.e., $T$ satisfies `IsTraceClass T`), this function returns $T$ as an element of the trace-class Banach space $\mathcal{S}_1(H)$.

Let $H$ be a complex Hilbert space and $\mathcal{B}(H)$ be the space of bounded linear operators on $H$. For any operator $T \in \mathcal{B}(H)$ that is trace-class, the underlying bounded linear operator of the element in the trace-class space $\mathcal{S}_1(H)$ constructed from $T$ (via `ofOperator`) is equal to $T$.

Let $H$ be a complex Hilbert space and let $\mathcal{S}_1(H)$ be the space of trace-class operators on $H$. The trace norm $\|\cdot\|_1$ satisfies the axioms of an additive group norm (`AddGroupNorm`) on $\mathcal{S}_1(H)$. Specifically, for all operators $T, T' \in \mathcal{S}_1(H)$, the following properties hold: - **Identity**: $\|0\|_1 = 0$. - **Negation**: $\|-T\|_1 = \|T\|_1$. - **Triangle Inequality**: $\|T + T'\|_1 \leq \|T\|_1 + \|T'\|_1$. - **Definiteness**: $\|T\|_1 = 0$ implies $T = 0$. This is established by the fact that the operator norm is dominated by the trace norm ($\|T\| \leq \|T\|_1$), so if the trace norm vanishes, the operator itself must be zero.

Let $H$ be a complex Hilbert space. The space of trace-class operators $\mathcal{S}_1(H)$ is a normed additive abelian group, where the norm of an operator $T \in \mathcal{S}_1(H)$ is defined as the trace norm $\|T\|_1$.

Let $H$ be a complex Hilbert space and let $\mathcal{S}_1(H)$ denote the Banach space of trace-class operators on $H$. For any operator $T \in \mathcal{S}_1(H)$, the norm $\|T\|$ in the space $\mathcal{S}_1(H)$ is equal to the trace norm $\|T\|_1$.

Let $H$ be a complex Hilbert space. The space of trace-class operators $\mathcal{S}_1(H)$ is a normed space over the field of complex numbers $\mathbb{C}$ with respect to the trace norm $\|\cdot\|_1$. This structure implies that scalar multiplication is compatible with the norm, such that for any $c \in \mathbb{C}$ and $T \in \mathcal{S}_1(H)$, the identity $\|c T\|_1 = |c| \|T\|_1$ holds.

Let $H$ be a Hilbert space. Let $(T_n)_{n \in \mathbb{N}}$ be a sequence of continuous linear operators on $H$, and let $T$ be a continuous linear operator on $H$. Suppose that for every $n$, $T_n$ is a trace-class operator whose trace norm is bounded by a constant $C$ (i.e., $\|T_n\|_1 \le C$ for all $n$). If $T_n$ converges to $T$ in the operator norm as $n \to \infty$, then $T$ is also a trace-class operator and its trace norm satisfies $\|T\|_1 \le C$.

Let $H$ be a complex Hilbert space. The space of trace-class operators $\mathcal{S}_1(H)$ on $H$, equipped with the trace norm $\|\cdot\|_1$, is a complete metric space. Consequently, since $\mathcal{S}_1(H)$ is a normed space, it is a Banach space.