Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Quantum Information Measures

1 · Prerequisites

2 · Summary

This page defines finite-dimensional von Neumann entropy, support-sensitive quantum relative entropy, quantum mutual and conditional information, and classical-quantum ensembles under the library's linear-first inner-product convention and natural-log nats units. It proves the finite entropy identities and Holevo identity, joint convexity and partial-trace/channel data processing for quantum relative entropy, its nonnegativity with equality exactly for equal states, and the finite Holevo measurement bound. Conditional entropy and conditional mutual information are given as entropy-form definitions; no nonnegativity claim for either is included.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite-dimensional von Neumann entropy

Definition

Let $H$ be a nonzero finite-dimensional complex inner-product space, with the root convention that its inner product is linear in the first argument, and let $ρ$ be a density operator on $H$ (Density operator). If $λ_{1}, \dots, λ_{d}$ are its eigenvalues counted with multiplicity, define its von Neumann entropy by

$S (ρ) : = - tr (ρ \ln ρ) : = - \sum_{j : λ_{j} > 0} λ_{j} \ln λ_{j} .$

The trace is the finite-dimensional endomorphism trace (The basis-independent trace of an endomorphism of a finite-dimensional vector space), and the spectral definition makes the expression independent of the eigenbasis. The term for a zero eigenvalue is defined to be $0 \ln 0 : = 0$ . The default unit is nats, using the natural logarithm (The natural logarithm as the inverse of the exponential function); the entropy in bits is $S_{2} (ρ) : = S (ρ) / \ln 2$ .

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Partial traces of a finite bipartite state are states

Statement

For nonzero finite-dimensional complex inner-product spaces $H_{A}, H_{B}$ and a density operator $ρ_{A B}$ on $H_{A} \otimes H_{B}$ , both marginals $ρ_{A} : = {Tr}_{B} ρ_{A B}$ and $ρ_{B} : = {Tr}_{A} ρ_{A B}$ are density operators.

Facts & Assumptions

Given: The spaces $H_{A}, H_{B}$ and the state $ρ_{A B}$ in the Statement.

[F1]

Density operator: a density operator is non-negative and has trace one.

[F2]

Partial trace over a finite tensor factor: in ordered orthonormal bases, $({Tr}_{B} R)_{i i^{'}} = \sum_{j} R_{(i, j), (i^{'}, j)}$ .

[F3]

Partial trace over the first tensor factor: in ordered orthonormal bases, $({Tr}_{A} R)_{j j^{'}} = \sum_{i} R_{(i, j), (i, j^{'})}$ .

[F4]

The partial trace preserves non-negativity and total trace: the partial trace over a finite second tensor factor preserves non-negativity and total trace.

[F5]

Non-negative and positive operators: non-negative means self-adjoint with nonnegative quadratic form.

[F6]

Ordered tensor registers, their inner product, and wire permutations: the product inner product and product basis respect the displayed tensor-factor order.

[F7]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

[F8]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: trace is the sum of diagonal entries in an ordered basis.

Proof

1.1givenF1F2F4

By the second-factor formula [F2] and the positivity/trace theorem [F4], $ρ_{A} = {Tr}_{B} ρ_{A B}$ is non-negative and has trace $tr (ρ_{A B}) = 1$ . It is therefore a density operator by [F1].

1.2givenF1F3F5F6F7choosealgebra

Choose ordered orthonormal bases $(a_{i})$ and $(b_{j})$ of $H_{A}, H_{B}$ by [F7]. Formula [F3] and the product inner product in [F6] give $⟨ ρ_{B} y, y ⟩ = \sum_{i} ⟨ ρ_{A B} (a_{i} \otimes y), a_{i} \otimes y ⟩$ for every $y \in H_{B}$ ; every summand is nonnegative by [F1] and [F5]. The matrix formula [F3] also shows $ρ_{B}$ is self-adjoint because $ρ_{A B}$ is self-adjoint. Hence $ρ_{B}$ is non-negative.

2.1givenF1F3F8step 1.2algebra∎

Summing the diagonal entries in [F3] gives $tr (ρ_{B}) = \sum_{i, j} (ρ_{A B})_{(i, j), (i, j)} = tr (ρ_{A B}) = 1$ by [F8] and [F1]. Therefore $ρ_{B}$ is a density operator by [F1].

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

An orthogonal finite ensemble block sum is a density operator

Statement

Let $X$ be a finite nonempty set, identify its labels with the computational orthonormal basis $(ξ_{x})_{x \in X}$ of a register $H_{X}$ (Finite registers and their ordered computational bases), and define the orthogonal rank-one projection $Π_{x} : H_{X} \to H_{X}$ by $Π_{x} z : = ⟨ z, ξ_{x} ⟩ ξ_{x}$ under the root linear-first convention. Let $H_{B}$ be a nonzero finite-dimensional complex inner-product space. For probabilities $p_{x} \geq 0$ with $\sum_{x \in X} p_{x} = 1$ and density operators $ρ_{x}$ on $H_{B}$ , the operator

$ρ_{X B} : = \sum_{x \in X} p_{x} Π_{x} \otimes ρ_{x}$

is a density operator on $H_{X} \otimes H_{B}$ .

Facts & Assumptions

Given: The finite label set $X$ , the register $H_{X}$ , the space $H_{B}$ , the probability vector $(p_{x})$ , and the density operators $(ρ_{x})$ in the Statement.

[F1]

Finite registers and their ordered computational bases: the computational vectors $(ξ_{x})$ form an orthonormal basis of their finite register.

[F2]

Density operator: each $ρ_{x}$ is non-negative with trace one.

[F3]

Ordered tensor registers, their inner product, and wire permutations: the tensor product carries the product inner product and the displayed factor order.

[F4]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: a non-negative operator is self-adjoint with nonnegative quadratic form.

[F5]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: trace is the sum of diagonal entries in any ordered basis.

Proof

1.1givenF1F2F3F4algebra

Every $v \in H_{X} \otimes H_{B}$ has a unique form $v = \sum_{x \in X} ξ_{x} \otimes v_{x}$ . Orthonormality in [F1] and the product inner product in [F3] give $⟨ ρ_{X B} v, v ⟩ = \sum_{x} p_{x} ⟨ ρ_{x} v_{x}, v_{x} ⟩ \geq 0$ by [F2]. In the same product basis $ρ_{X B}$ is block diagonal with self-adjoint blocks $p_{x} ρ_{x}$ , so it is self-adjoint and non-negative by [F4].

2.1givenF2F5step 1.1algebra∎

By [F5], $tr (ρ_{X B}) = \sum_{x} p_{x} tr (ρ_{x}) = \sum_{x} p_{x} = 1$ . Thus $ρ_{X B}$ is a density operator by [F2].

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Inverse compression for positive resolvents

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces, let $T : K \to K$ be positive definite, and let $V : H \to K$ satisfy $V^{*} V = I_{H}$ . For every $s \geq 0$ ,

$V^{*} (T + s I_{K})^{- 1} V ⪰ (V^{*} T V + s I_{H})^{- 1},$

where $A ⪰ B$ means that $A - B$ is non-negative. If $H = {0}$ , both sides are the unique endomorphism of $H$ .

Facts & Assumptions

Given: The spaces $H, K$ , the positive definite operator $T$ , the isometry $V$ , and $s \geq 0$ in the Statement.

[F1]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument, conjugate-linear in its second, and positive definite.

[F2]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ V x, z ⟩ = ⟨ x, V^{*} z ⟩$ .

[F3]

Non-negative and positive operators: positive definiteness means self-adjointness and strictly positive quadratic form on nonzero vectors.

[F4]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: non-negative operators are self-adjoint with nonnegative quadratic form.

[F5]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: every linear map between finite-dimensional inner-product spaces has a unique linear adjoint, including zero-dimensional spaces.

Proof

1.1givenF5F1F2F3algebra

All adjoints of the finite-dimensional linear maps used below exist uniquely by [F5]. Let $C$ be positive definite on a finite-dimensional space and $y$ any vector. The operator $C$ is injective by [F3], hence invertible in finite dimension; put $z_{0} = C^{- 1} y$ . Expanding with [F1]–[F2] gives $2 Re ⟨ y, z ⟩ - ⟨ C z, z ⟩ = ⟨ C^{- 1} y, y ⟩ - ⟨ C (z - z_{0}), z - z_{0} ⟩$ . The last term is nonnegative by [F3] and vanishes at $z = z_{0}$ , so $⟨ C^{- 1} y, y ⟩ = \max_{z} {2 Re ⟨ y, z ⟩ - ⟨ C z, z ⟩}$ .

2.1givenF2F3F4step 1.1algebra∎

If $H = {0}$ the assertion is immediate. Otherwise fix $x \in H$ , put $C = T + s I_{K}$ and $y = V x$ . By [F2] and $V^{*} V = I_{H}$ , $V^{*} C V = V^{*} T V + s I_{H}$ , which is positive definite. Restrict the maximum in step 1.1 to $z = V w$ ; the isometry identity gives $⟨ V x, V w ⟩ = ⟨ x, w ⟩$ and $⟨ C V w, V w ⟩ = ⟨ (V^{*} T V + s I_{H}) w, w ⟩$ . Hence $⟨ (T + s I_{K})^{- 1} V x, V x ⟩ \geq ⟨ (V^{*} T V + s I_{H})^{- 1} x, x ⟩$ . This holds for every $x$ , so the self-adjoint operator difference is non-negative by [F4], proving the order inequality.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Nonnegativity and equality for finite classical relative entropy

Statement

For probability vectors $p = (p_{i})_{i \in I}$ and $q = (q_{i})_{i \in I}$ on a finite nonempty set $I$ , define

$D (p ∥ q) : = {\begin{cases} \sum_{i : p_{i} > 0} p_{i} \ln \frac{p_{i}}{q_{i}}, & p_{i} > 0 \Rightarrow q_{i} > 0, \\ + \infty, & otherwise. \end{cases}$

Then $D (p ∥ q) \geq 0$ , and $D (p ∥ q) = 0$ if and only if $p = q$ .

Facts & Assumptions

Given: The finite set $I$ and probability vectors $p, q$ in the Statement.

[F1]

The natural logarithm as the inverse of the exponential function: $\ln x$ is the inverse exponential on $(0, \infty)$ .

[F2]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln$ is strictly increasing, continuous, and $\ln 1 = 0$ .

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $(\ln x)^{'} = 1 / x$ for $x > 0$ .

[F4]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a function continuous on a closed interval and differentiable inside, some interior derivative equals the endpoint slope.

Proof

1.1givenF1F2F3F4casesalgebra

Set $g (t) = t - 1 - \ln t$ for $t > 0$ . For $t > 1$ , [F3] and [F4] give $g (t) - g (1) = g^{'} (c) (t - 1)$ for some $c \in (1, t)$ , where $g^{'} (c) = 1 - 1 / c > 0$ ; for $0 < t < 1$ , they give $g (1) - g (t) = g^{'} (c) (1 - t)$ for some $c \in (t, 1)$ , where $g^{'} (c) = 1 - 1 / c < 0$ . Thus $g (t) > 0$ unless $t = 1$ , when $g (1) = 0$ . Equivalently, $- \ln t \geq 1 - t$ , with equality only at $t = 1$ .

2.1givenstep 1.1algebracases∎

If $p_{i} > 0 = q_{i}$ for some $i$ , then $D (p ∥ q) = + \infty$ by definition. Otherwise, for each $i$ with $p_{i} > 0$ , apply step 1.1 to $t = q_{i} / p_{i}$ and multiply by $p_{i}$ , obtaining $p_{i} \ln (p_{i} / q_{i}) \geq p_{i} - q_{i}$ . Summing gives $D (p ∥ q) \geq 1 - \sum_{i : p_{i} > 0} q_{i} \geq 0$ . Equality forces $q_{i} = p_{i}$ on the positive support by step 1.1 and no $q$ -mass outside it by the final inequality; hence $p = q$ . Conversely, $p = q$ makes every summand zero.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

A finite POVM defines a classical-output quantum channel

Statement

Let $H$ be a nonzero finite-dimensional complex inner-product space and let $(E_{y})_{y \in Ω}$ be a finite POVM on $H$ , where $Ω = {y_{0}, \dots, y_{m - 1}}$ is a fixed enumeration of its nonempty outcome set. Let $K = C^{m}$ with standard orthonormal basis $(f_{0}, \dots, f_{m - 1})$ , and set $Π_{j} z : = ⟨ z, f_{j} ⟩ f_{j}$ , the rank-one projection onto $f_{j}$ under the root linear-first convention. The map $M_{E} (X) : = \sum_{j < m} tr (X E_{y_{j}}) Π_{j}$ is a quantum channel from $H$ to $K$ . For the indexed register $C^{Ω}$ with orthonormal basis $∣ y ⟩$ , the unitary identification $J f_{j} = ∣ y_{j} ⟩$ gives the equivalent channel $X \mapsto \sum_{y \in Ω} tr (E_{y} X) ∣ y ⟩ ⟨ y ∣ = J M_{E} (X) J^{*}$ . Thus either finite outcome-register convention is covered.

Facts & Assumptions

Given: The space $H$ , the finite POVM, its enumeration, and the output register $K$ in the Statement.

[F1]

Finite POVMs and their outcome law: each $E_{y}$ is non-negative and $\sum_{y} E_{y} = I_{H}$ ; the outcome weight on a state $ρ$ is $tr (ρ E_{y})$ .

[F2]

A non-negative operator has a unique non-negative square root: every non-negative operator $E_{y}$ has a non-negative square root $E_{y}^{1 / 2}$ .

[F3]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument and conjugate-linear in its second.

[F4]

Finite Kraus representation: a finite Kraus family represents $Φ$ when $Φ (X) = \sum_{a} K_{a} X K_{a}^{*}$ for every input operator.

[F5]

Kraus and Choi characterizations of complete positivity: a finite Kraus representation implies complete positivity.

[F6]

Trace preservation is Kraus normalization: a finite Kraus representation is trace-preserving exactly when $\sum_{a} K_{a}^{*} K_{a} = I_{H}$ .

[F7]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : the trace is cyclic for compatible finite-dimensional maps.

[F8]

Finite-dimensional quantum channel: a finite-dimensional quantum channel is a complex-linear completely positive trace-preserving map on the full operator space.

[F9]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : the adjoint satisfies $⟨ K x, z ⟩ = ⟨ x, K^{*} z ⟩$ .

[F10]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

[F11]

Finite registers and their ordered computational bases: the specified output basis $(f_{j})$ is orthonormal.

[F12]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: finite-dimensional linear maps have unique adjoints.

Proof

1.1givenF12F2F3F9F10F11constructchoose

The adjoints used below exist uniquely by [F12]. Choose an ordered orthonormal basis $(e_{k})_{k < d}$ of $H$ using [F10]. For each $j < m$ and $k < d$ , define $K_{j k} : H \to K$ by $K_{j k} x = f_{j} ⟨ E_{y_{j}}^{1 / 2} x, e_{k} ⟩$ . This is linear by the root convention in [F3]. Set $P_{k} x : = ⟨ x, e_{k} ⟩ e_{k}$ . The adjoint identity [F9] and the output-basis orthonormality [F11] give $K_{j k}^{*} z = ⟨ z, f_{j} ⟩ E_{y_{j}}^{1 / 2} e_{k}$ and therefore $K_{j k}^{*} K_{j k} = E_{y_{j}}^{1 / 2} P_{k} E_{y_{j}}^{1 / 2}$ .

2.1givenF1F2F6step 1.1algebra

Since $(e_{k})$ is a basis, $\sum_{k} P_{k} = I_{H}$ . Using step 1.1 and the completeness relation in [F1], $\sum_{j, k} K_{j k}^{*} K_{j k} = \sum_{j} E_{y_{j}}^{1 / 2} (\sum_{k} P_{k}) E_{y_{j}}^{1 / 2} = \sum_{j} E_{y_{j}} = I_{H}$ . Thus the finite family is trace-preserving by [F6].

3.1givenF4F6F5F7F8F11step 1.1step 2.1algebra∎

For each fixed $j$ , the $f_{j}$ output diagonal entry of $\sum_{k} K_{j k} X K_{j k}^{*}$ is $\sum_{k} ⟨ E_{y_{j}}^{1 / 2} X E_{y_{j}}^{1 / 2} e_{k}, e_{k} ⟩ = tr (E_{y_{j}}^{1 / 2} X E_{y_{j}}^{1 / 2})$ . By trace cyclicity [F7], this is $tr (X E_{y_{j}})$ , and all off-diagonal output entries vanish because each $K_{j k}$ has range in $C f_{j}$ and [F11] makes the output basis orthonormal. Summing over $j$ yields $M_{E}$ , so it has the finite Kraus representation [F4] and is completely positive by [F5]. Together with steps 1.1 and 2.1 it is a quantum channel by [F8]. The coordinate map $J f_{j} = ∣ y_{j} ⟩$ is unitary because it carries one orthonormal basis onto the other; replacing each Kraus map by $J K_{j k}$ preserves its normalization and complete positivity by [F5]–[F6]. The conjugated output is $\sum_{j} tr (X E_{y_{j}}) ∣ y_{j} ⟩ ⟨ y_{j} ∣ = \sum_{y} tr (E_{y} X) ∣ y ⟩ ⟨ y ∣$ by [F7], proving the indexed-register clause.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite-dimensional quantum relative entropy

Definition

Let $H$ be a finite-dimensional complex inner-product space and let $A, B : H \to H$ be non-negative operators. For such an operator $A$ , set $supp (A) : = (\ker A)^{⊥}$ , where $\ker A$ is the kernel of a linear map (Kernel and image of a linear map); this extends the density-operator support convention in Density operator. If $supp (A) \subseteq supp (B)$ , define

$D (A ∥ B) : = tr (A \ln A) - tr (A \ln B) .$

Here $\ln A$ is defined spectrally on the positive eigenspaces of $A$ with $0 \ln 0 : = 0$ , and $\ln B$ in the cross term is restricted to $supp (B)$ ; the support condition ensures that $A$ vanishes on $\ker B$ , so the omitted kernel contributes zero. If $supp (A) ⊈ supp (B)$ , set $D (A ∥ B) : = + \infty$ . In particular, $D (0 ∥ B) = 0$ . For density operators this is the finite-dimensional quantum relative entropy. The logarithms are natural, so the value is in nats; the base-two value is $D_{2} (A ∥ B) : = D (A ∥ B) / \ln 2$ .

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite quantum mutual, conditional, and conditional mutual information

Definition

For a finite bipartite state $ρ_{A B}$ on the ordered product $H_{A} \otimes H_{B}$ , write $ρ_{A} = {Tr}_{B} ρ_{A B}$ and $ρ_{B} = {Tr}_{A} ρ_{A B}$ , using the partial traces in Partial trace over a finite tensor factor and Partial trace over the first tensor factor. They are states by Partial traces of a finite bipartite state are states. Define

$S (A)_{ρ} : = S (ρ_{A}), S (A ∣ B)_{ρ} : = S (ρ_{A B}) - S (ρ_{B}), I (A : B)_{ρ} : = S (ρ_{A}) + S (ρ_{B}) - S (ρ_{A B}) .$

For a finite tripartite state $ρ_{A B C}$ on the ordered product $H_{A} \otimes H_{B} \otimes H_{C}$ , set $ρ_{A B} : = {Tr}_{H_{C}} ρ_{A B C}$ after identifying the factors as $(H_{A} \otimes H_{B}) \otimes H_{C}$ , and $ρ_{B C} : = {Tr}_{H_{A}} ρ_{A B C}$ after identifying them as $H_{A} \otimes (H_{B} \otimes H_{C})$ . Let $P : H_{A} \otimes H_{B} \otimes H_{C} \to H_{A} \otimes H_{C} \otimes H_{B}$ be the wire permutation taking factor order $A, B, C$ to $A, C, B$ (Ordered tensor registers, their inner product, and wire permutations, Finite wire permutations are unitary basis permutations) whose unique adjoint $P^{*}$ exists by Every linear map between finite-dimensional inner product spaces has a unique adjoint, and set $ρ_{A C} : = {Tr}_{H_{B}} (P ρ_{A B C} P^{*})$ , tracing out the last factor. Because $P$ is unitary, $P ρ_{A B C} P^{*}$ is a state: unitary conjugation preserves non-negativity by the adjoint identity (The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ , Non-negative and positive operators) and preserves trace by cyclicity (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ ). Finally set $ρ_{C} : = {Tr}_{H_{B}} ρ_{B C}$ . All these marginals are density operators by applying Partial traces of a finite bipartite state are states after grouping factors. Define

$I (A : B ∣ C)_{ρ} : = S (ρ_{A C}) + S (ρ_{B C}) - S (ρ_{C}) - S (ρ_{A B C}) .$

These are finite-dimensional definitions only; no non-negativity of conditional entropy or conditional mutual information is part of the notation.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

The compression Jensen inequality for the negative logarithm

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces, let $T : K \to K$ be positive definite, and let $V : H \to K$ satisfy $V^{*} V = I_{H}$ . Then, in the non-negative operator order,

$- \ln (V^{*} T V) ⪯ V^{*} (- \ln T) V,$

where $R ⪯ S$ means $S - R$ is non-negative and logarithms of positive-definite operators are defined by finite spectral calculus.

Facts & Assumptions

Given: $H, K, T, V$ as in the Statement.

[F1]

Inverse compression for positive resolvents: $V^{*} (T + s I_{K})^{- 1} V ⪰ (V^{*} T V + s I_{H})^{- 1}$ for every $s \geq 0$ .

[F2]

The natural logarithm as the inverse of the exponential function and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: the natural logarithm is defined on positive reals and has derivative $1 / t$ .

[F3]

Non-negative and positive operators: a non-negative operator is self-adjoint with nonnegative quadratic form.

[F4]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the natural logarithm is continuous on positive reals, has $\ln 1 = 0$ , and obeys $\ln (u / v) = \ln u - \ln v$ .

[F5]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: every real continuous function on a compact interval is Riemann integrable.

[F6]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : an everywhere differentiable primitive on a closed interval, including one-sided endpoint derivatives, with integrable derivative has derivative integral equal to its endpoint increment.

[F7]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: positive-definite finite-dimensional operators have orthonormal eigenbases with strictly positive eigenvalues.

Proof

1.1givenF2F4F5F6F7algebra

For $t > 0$ and $R > 0$ , set $F_{t} (s) = \ln (t + s) - \ln (1 + s)$ on $s > - \min (t, 1)$ . Translated difference quotients in [F2] give $F_{t}^{'} (s) = (t + s)^{- 1} - (1 + s)^{- 1}$ , including the one-sided derivatives on $[0, R]$ . For $s, u \in [0, R]$ , $∣ (t + s)^{- 1} - (t + u)^{- 1} ∣ \leq ∣ s - u ∣ / t^{2}$ and $∣ (1 + s)^{- 1} - (1 + u)^{- 1} ∣ \leq ∣ s - u ∣$ , so the derivative is continuous and integrable by [F5]. Thus [F6] and [F4] give $\int_{0}^{R} ((t + s)^{- 1} - (1 + s)^{- 1}) d s = \ln ((t + R) / (1 + R)) - \ln t$ . As $R \to \infty$ , the quotient tends to $1$ , so [F4] gives the limit $- \ln t$ (also when $t = 1$ ). Applying this scalar identity to each of the finitely many positive eigenvalues in [F7] yields the corresponding operator integral identity in norm, since the maximum of finitely many scalar errors tends to zero. On a zero-dimensional space the empty spectral formula is the unique endomorphism, so the same assertion is vacuous and valid.

2.1givenF1F3step 1.1algebra∎

Since $V^{*} V = I_{H}$ and $T$ is positive definite, $V^{*} T V$ is positive definite on nonzero $H$ : for $x \neq 0$ , $V x \neq 0$ and $⟨ V^{*} T V x, x ⟩ = ⟨ T V x, V x ⟩ > 0$ . Apply [F1] at each $s \geq 0$ . Subtracting $(1 + s)^{- 1} I_{H}$ preserves the order inequality. For every $x$ , integrating the resulting quadratic-form inequality over $[0, R]$ gives a non-negative quadratic form; the operator norm limits as $R \to \infty$ exist by step 1.1, and the limit remains non-negative because quadratic forms are continuous. The limit is $- \ln (V^{*} T V) ⪯ V^{*} (- \ln T) V$ , as required.

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Finite classical-quantum states and Holevo information

Definition

Let $X$ be a finite nonempty classical label set, represented by a register $H_{X}$ with computational orthonormal basis $(ξ_{x})_{x \in X}$ (Finite registers and their ordered computational bases). For each $x$ , write $Π_{x} z : = ⟨ z, ξ_{x} ⟩ ξ_{x}$ , the rank-one orthogonal projection using the root linear-first convention, as in An orthogonal finite ensemble block sum is a density operator. Let $H_{B}$ be a nonzero finite-dimensional complex inner-product space. A finite classical-quantum state is

$ρ_{X B} : = \sum_{x \in X} p_{x} Π_{x} \otimes ρ_{x},$

where $p_{x} \geq 0$ , $\sum_{x} p_{x} = 1$ , and each $ρ_{x}$ is a density operator on $H_{B}$ . It is a density operator by An orthogonal finite ensemble block sum is a density operator. Its quantum marginal is ${\overset{ˉ}{ρ}}_{B} : = \sum_{x} p_{x} ρ_{x} = {Tr}_{X} ρ_{X B}$ by the first-factor partial-trace formula in Partial trace over the first tensor factor, and it is a density operator by Partial traces of a finite bipartite state are states. The Holevo information of this ensemble is

$χ ({p_{x}, ρ_{x}}_{x \in X}) : = S ({\overset{ˉ}{ρ}}_{B}) - \sum_{x : p_{x} > 0} p_{x} S (ρ_{x}),$

where zero-probability branches contribute nothing. This is measured in nats under Finite-dimensional von Neumann entropy.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Joint state support is contained in the tensor product of its marginal supports

Statement

For a state $ρ_{A B}$ on a finite-dimensional bipartite space, with marginals $ρ_{A} = {Tr}_{B} ρ_{A B}$ and $ρ_{B} = {Tr}_{A} ρ_{A B}$ ,

$supp (ρ_{A B}) \subseteq supp (ρ_{A}) \otimes supp (ρ_{B}) = supp (ρ_{A} \otimes ρ_{B}) .$

Consequently $D (ρ_{A B} ∥ ρ_{A} \otimes ρ_{B})$ is finite.

Facts & Assumptions

Given: A finite-dimensional bipartite density operator $ρ_{A B}$ and the partial traces in the Statement.

[F1]

Finite-dimensional quantum relative entropy: for every non-negative operator $R$ , $supp (R) = (\ker R)^{⊥}$ ; support inclusion is the finiteness condition for $D$ .

[F2]

Partial trace over a finite tensor factor: the second-factor marginal has entries $(ρ_{A})_{i i^{'}} = \sum_{j} (ρ_{A B})_{(i, j), (i^{'}, j)}$ .

[F3]

Partial trace over the first tensor factor: the first-factor marginal has entries $(ρ_{B})_{j j^{'}} = \sum_{i} (ρ_{A B})_{(i, j), (i, j^{'})}$ .

[F4]

Partial traces of a finite bipartite state are states: both marginals are density operators.

[F5]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: every non-negative operator has a factorization $R = S^{*} S$ , so zero quadratic form at $v$ implies $R v = 0$ .

[F6]

[F7]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

Proof

1.1givenF1F2F5F7choosealgebra

Choose an orthonormal basis $(b_{j})$ of $H_{B}$ using [F7]. If $u \in \ker ρ_{A}$ , then [F2] gives $0 = ⟨ ρ_{A} u, u ⟩ = \sum_{j} ⟨ ρ_{A B} (u \otimes b_{j}), u \otimes b_{j} ⟩$ . Every term is nonnegative by [F1], so every term is zero. By [F5], write $ρ_{A B} = S^{*} S$ ; a zero quadratic form then gives $S (u \otimes b_{j}) = 0$ and hence $ρ_{A B} (u \otimes b_{j}) = 0$ . Since $(b_{j})$ spans $H_{B}$ , $ρ_{A B}$ annihilates $\ker ρ_{A} \otimes H_{B}$ .

1.2givenF1F3F5F7choosealgebra

Choose an orthonormal basis $(a_{i})$ of $H_{A}$ using [F7]. If $v \in \ker ρ_{B}$ , then [F3] similarly gives $0 = ⟨ ρ_{B} v, v ⟩ = \sum_{i} ⟨ ρ_{A B} (a_{i} \otimes v), a_{i} \otimes v ⟩$ . Positivity and [F5] show that $ρ_{A B}$ annihilates $H_{A} \otimes \ker ρ_{B}$ .

2.1F1F4F6step 1.1step 1.2algebra∎

Self-adjointness of $ρ_{A B}$ implies its range is orthogonal to both subspaces annihilated in steps 1.1 and 1.2. Using the orthogonal decompositions $H_{A} = supp (ρ_{A}) \oplus \ker ρ_{A}$ and $H_{B} = supp (ρ_{B}) \oplus \ker ρ_{B}$ , the intersection of their orthogonal complements is $supp (ρ_{A}) \otimes supp (ρ_{B})$ . For non-negative $ρ_{A B}$ its range equals its support by [F6]. The product spectral decomposition also gives $supp (ρ_{A} \otimes ρ_{B}) = supp (ρ_{A}) \otimes supp (ρ_{B})$ . Hence the stated inclusion holds, and [F1] makes the divergence finite.

LemmaStatement: Literature-sourcedProof: AI-generatedOpen item page →

Relative modular representation of finite quantum relative entropy

Statement

Let $A, B$ be positive-definite operators on a nonzero finite-dimensional complex inner-product space $H$ . On $L (H)$ , with Hilbert-Schmidt inner product $⟨ X, Y ⟩_{H S} : = tr (X Y^{*})$ , define $Δ_{B, A} (X) : = B X A^{- 1}$ . Then $Δ_{B, A}$ is positive definite and

$D (A ∥ B) = ⟨ (- \ln Δ_{B, A}) (A^{1 / 2}), A^{1 / 2} ⟩_{H S} .$

The logarithm of $Δ_{B, A}$ is defined by its positive eigenvalues.

Facts & Assumptions

Given: $H, A, B$ as in the Statement.

[F1]

Finite-dimensional quantum relative entropy: for positive-definite $A, B$ , $D (A ∥ B) = tr (A \ln A) - tr (A \ln B)$ .

[F2]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: positive-definite operators have orthonormal eigenbases with positive eigenvalues.

[F3]

A non-negative operator has a unique non-negative square root: $A$ has a positive-definite square root $A^{1 / 2}$ .

[F4]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is cyclic for compatible finite-dimensional maps.

[F5]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument and conjugate-linear in its second, so $E_{j i} x = ⟨ x, u_{i} ⟩ v_{j}$ is linear.

[F6]

[F7]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : the adjoint is characterized by $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ .

[F8]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: for positive real $x, y$ , $\ln (x / y) = \ln x - \ln y$ .

Proof

1.1givenF6F7F8F2F5algebrachoose

All adjoints of the finite-dimensional linear maps used below exist uniquely by [F6]. Choose orthonormal eigenbases $(u_{i})$ and $(v_{j})$ for $A$ and $B$ , with $A u_{i} = a_{i} u_{i}$ , $B v_{j} = b_{j} v_{j}$ and $a_{i}, b_{j} > 0$ , using [F2]. For each $i, j$ define $E_{j i} x : = ⟨ x, u_{i} ⟩ v_{j}$ . These linear matrix units form an orthonormal basis of $L (H)$ for $⟨ \cdot, \cdot ⟩_{H S}$ by the adjoint pairing [F7] and direct trace evaluation. They satisfy $B E_{j i} = b_{j} E_{j i}$ and $E_{j i} A^{- 1} = a_{i}^{- 1} E_{j i}$ , so $Δ_{B, A} E_{j i} = (b_{j} / a_{i}) E_{j i}$ . The quotient law [F8] gives $- \ln (b_{j} / a_{i}) = - \ln b_{j} + \ln a_{i}$ , so spectral calculus on this basis shows that $Δ_{B, A}$ is positive definite and gives $(- \ln Δ_{B, A}) (X) = - (\ln B) X + X (\ln A)$ .

2.1F1F3F4step 1.1algebra∎

Applying the formula in step 1.1 to $A^{1 / 2}$ gives $⟨ (- \ln Δ_{B, A}) (A^{1 / 2}), A^{1 / 2} ⟩_{H S} = tr (- A \ln B + A^{1 / 2} (\ln A) A^{1 / 2})$ . By trace cyclicity [F4], the second trace is $tr (A \ln A)$ . The result equals $D (A ∥ B)$ by [F1], proving the identity.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Support-sensitive regularization limit for quantum relative entropy

Statement

For non-negative $A, B$ on a finite-dimensional complex inner-product space,

$\lim_{ε ↓ 0} D (A + ε I ∥ B + ε I) = D (A ∥ B),$

where the right side may be $+ \infty$ under the support convention of Finite-dimensional quantum relative entropy.

Facts & Assumptions

Given: The finite-dimensional non-negative operators $A, B$ in the Statement.

[F1]

Finite-dimensional quantum relative entropy: $D (A ∥ B)$ is finite exactly when $supp (A) \subseteq supp (B)$ , and on that branch it is the difference of the two spectral logarithmic traces.

[F2]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: $A, B$ have orthonormal eigenbases with nonnegative eigenvalues.

[F3]

A non-negative operator has a unique non-negative square root: $⟨ A v, v ⟩ = ∥ A^{1 / 2} v ∥^{2}$ , so zero quadratic form for a non-negative operator implies it annihilates the vector.

[F4]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the natural logarithm is strictly increasing and onto $R$ . For every real $M$ , choose $u > 0$ with $\ln u < M$ ; then $0 < t < u$ implies $\ln t < M$ , so $\ln t \to - \infty$ as $t ↓ 0$ .

[F5]

The natural logarithm is bounded above by its positive argument minus one: for $x \geq 1$ , $0 \leq \ln x \leq x - 1$ .

Proof

1.1givenF1F2F4F5algebrachoose

First suppose $supp (A) \subseteq supp (B)$ , so $\ker B \subseteq \ker A$ . Choose an orthonormal eigenbasis $(e_{j})$ of $B$ with eigenvalues $b_{j} \geq 0$ , and put $a_{j} : = ⟨ A e_{j}, e_{j} ⟩ \geq 0$ . If $b_{j} = 0$ , then $e_{j} \in \ker A$ , so $a_{j} = 0$ , and therefore $tr (A \ln (B + ε I)) = \sum_{j : b_{j} > 0} a_{j} \ln (b_{j} + ε) \to tr (A \ln B)$ . Also $ε tr (\ln (B + ε I)) \to 0$ : positive $b_{j}$ terms use continuity, while zero $b_{j}$ terms use $ε \ln ε \to 0$ . The latter follows from [F5]: for $0 < t \leq 1$ , put $u = t^{- 1 / 2} \geq 1$ . Then $0 \leq - t \ln t = 2 t \ln u \leq 2 t (u - 1) = 2 (\sqrt{t} - t) \to 0$ by applying the bound to $u$ . The same limit gives $t \ln t \to 0$ at zero, so $tr ((A + ε I) \ln (A + ε I)) \to tr (A \ln A)$ . Substituting these limits in the definition proves the claim in this support-inclusion case.

2.1givenF1F2F3F4F5step 1.1algebrachoose∎

Now suppose $supp (A) ⊈ supp (B)$ . There is a unit vector $e \in \ker B ∖ \ker A$ , so $a : = ⟨ A e, e ⟩ > 0$ by [F3]. Choose an orthonormal eigenbasis of $B$ containing a basis $(u_{k})$ of $\ker B$ . At least one coefficient $⟨ A u_{k}, u_{k} ⟩$ is positive: otherwise [F3] would give $A u_{k} = 0$ for every $k$ , hence $A e = 0$ . Therefore the sum $c : = \sum_{k} ⟨ A u_{k}, u_{k} ⟩$ is positive. In $tr (A \ln (B + ε I))$ , this coefficient multiplies $\ln ε \to - \infty$ , while terms from positive eigenvalues of $B$ remain bounded. The entropy trace $tr ((A + ε I) \ln (A + ε I))$ has a finite limit as in step 1.1, and the additional $ε tr (\ln (B + ε I))$ tends to zero by [F4]–[F5]. Therefore the relative entropy tends to $+ \infty$ , equal to the right side of the Statement.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Isometric invariance of finite quantum relative entropy

Statement

Let $V : H \to K$ be a linear map between finite-dimensional complex inner-product spaces satisfying $V^{*} V = I_{H}$ , and let $A, B$ be non-negative on $H$ . Then

$D (V A V^{*} ∥ V B V^{*}) = D (A ∥ B) .$

Facts & Assumptions

Given: $V, A, B$ as in the Statement.

[F1]

Finite-dimensional quantum relative entropy: support inclusion determines the finite branch of $D$ ; its value is computed from spectral logarithms on the supports.

[F2]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $V^{*} V = I_{H}$ implies $⟨ V x, V y ⟩ = ⟨ x, y ⟩$ for every $x, y \in H$ .

[F3]

[F4]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is cyclic for compatible finite-dimensional operators.

[F5]

Proof

1.1givenF5F2F3algebra

All adjoints of the finite-dimensional linear maps used below exist uniquely by [F5]. Let $M = ran V$ . Since $V$ is an isometry, it maps an orthonormal eigenbasis of $A$ to an orthonormal eigenbasis of $V A V^{*}$ on $M$ with the same nonzero eigenvalues; $V A V^{*}$ is zero on $M^{⊥}$ . The same holds for $B$ . Consequently $supp (V A V^{*}) = V (supp A)$ and $supp (V B V^{*}) = V (supp B)$ , so support inclusion holds on one side exactly when it holds on the other.

2.1givenF1F3F4step 1.1casesalgebra∎

On $M$ , spectral calculus gives $\ln (V A V^{*}) = V (\ln A) V^{*}$ on the positive support of $A$ , with the analogous identity for $B$ ; on $M^{⊥}$ both conjugated operators contribute zero to the support-restricted traces. Thus in the finite branch, cyclicity [F4] gives $tr (V A V^{*} \ln (V A V^{*})) = tr (A \ln A)$ and $tr (V A V^{*} \ln (V B V^{*})) = tr (A \ln B)$ . By [F1] their difference is $D (A ∥ B)$ . If support inclusion fails, step 1.1 shows both sides are $+ \infty$ by [F1].

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Finite quantum conditional mutual information identity

Statement

For every finite-dimensional tripartite state $ρ_{A B C}$ , the entropy-form conditional mutual information defined in Finite quantum mutual, conditional, and conditional mutual information satisfies

$I (A : B ∣ C)_{ρ} = I (A : B C)_{ρ} - I (A : C)_{ρ} .$

This is an algebraic identity; it asserts no non-negativity.

Facts & Assumptions

Given: A finite-dimensional tripartite density operator $ρ_{A B C}$ with the marginal conventions in Finite quantum mutual, conditional, and conditional mutual information.

[F1]

Finite quantum mutual, conditional, and conditional mutual information: $I (A : B ∣ C) = S (A C) + S (B C) - S (C) - S (A B C)$ and $I (A : B) = S (A) + S (B) - S (A B)$ .

Proof

1.1givenF1

By [F1], $I (A : B C)_{ρ} = S (A)_{ρ} + S (B C)_{ρ} - S (A B C)_{ρ}$ .

2.1givenF1step 1.1algebra∎

Also by [F1], $I (A : C)_{ρ} = S (A)_{ρ} + S (C)_{ρ} - S (A C)_{ρ}$ . Subtracting this from step 1.1 cancels $S (A)_{ρ}$ and gives $S (A C)_{ρ} + S (B C)_{ρ} - S (C)_{ρ} - S (A B C)_{ρ}$ , which is $I (A : B ∣ C)_{ρ}$ by [F1]. No inequality or non-negativity premise is used.

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Joint convexity of finite quantum relative entropy

Statement

Let $H$ be a finite-dimensional complex inner-product space, let $n \geq 1$ , let $A_{i}, B_{i} : H \to H$ be non-negative for $1 \leq i \leq n$ , and let $λ_{i} \geq 0$ with $\sum_{i} λ_{i} = 1$ . Then, in the extended-real order,

$D ⁣ (\sum_{i} λ_{i} A_{i} ∥ \sum_{i} λ_{i} B_{i}) \leq \sum_{i} λ_{i} D (A_{i} ∥ B_{i}),$

where zero-weight terms are omitted from the right side, and the order is that on the extended real line.

Facts & Assumptions

Given: $H$ , the finite families $(A_{i}), (B_{i})$ and the probability vector $(λ_{i})$ in the Statement.

[F1]

Finite-dimensional quantum relative entropy: for non-negative operators, $D$ is finite under support inclusion and uses natural spectral logarithms; otherwise it is $+ \infty$ .

[F2]

The compression Jensen inequality for the negative logarithm: $- \ln (V^{*} T V) ⪯ V^{*} (- \ln T) V$ for positive-definite $T$ and an isometry $V$ .

[F3]

Relative modular representation of finite quantum relative entropy: for positive-definite $A, B$ , $D (A ∥ B) = ⟨ (- \ln Δ_{B, A}) (A^{1 / 2}), A^{1 / 2} ⟩_{H S}$ with $Δ_{B, A} (X) = B X A^{- 1}$ .

[F4]

Support-sensitive regularization limit for quantum relative entropy: $D (A + ε I ∥ B + ε I) \to D (A ∥ B)$ as $ε ↓ 0$ , including the infinite support-failure branch.

[F5]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is cyclic for compatible finite-dimensional maps.

[F6]

A non-negative operator has a unique non-negative square root: each positive-definite $A$ has a positive-definite square root $A^{1 / 2}$ , hence an inverse square root.

[F7]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $U_{i}^{*}$ is characterized by $⟨ U_{i} X, Y ⟩ = ⟨ X, U_{i}^{*} Y ⟩$ .

[F8]

Proof

1.1givenF8F1F5F6F7algebracasesconstruct

All adjoints of the finite-dimensional linear maps used below exist uniquely by [F8]. Discard all indices with $λ_{i} = 0$ from both sides; at least one index remains because the weights sum to one. The remaining weights are strictly positive and still sum to one. If $H = {0}$ , all operators and relative entropies are zero by [F1], so the result holds. Now assume $H \neq {0}$ and first suppose every $A_{i}, B_{i}$ is positive definite. Set $A = \sum_{i} λ_{i} A_{i}$ and $B = \sum_{i} λ_{i} B_{i}$ . Positive-definite square roots and inverse square roots exist by [F6]. On the Hilbert-Schmidt spaces, with direct-sum inner product, define $U_{i} (X) : = \sqrt{λ_{i}} X A^{- 1 / 2} A_{i}^{1 / 2}$ and $U (X) : = (U_{i} (X))_{i}$ . Trace cyclicity [F5] and the adjoint definition [F7] in $⟨ U_{i} (X), Y ⟩_{H S}$ give $U_{i}^{*} (Y) = \sqrt{λ_{i}} Y A_{i}^{1 / 2} A^{- 1 / 2}$ . Therefore $U^{*} U (X) = X A^{- 1 / 2} (\sum_{i} λ_{i} A_{i}) A^{- 1 / 2} = X$ , so $U$ is an isometry.

2.1givenF2F3F6step 1.1algebra

Put $T : = ⨁_{i} Δ_{B_{i}, A_{i}}$ , positive definite by [F3]. For each $i$ , multiplication gives $U_{i}^{*} Δ_{B_{i}, A_{i}} U_{i} (X) = λ_{i} B_{i} X A^{- 1}$ , hence $U^{*} T U (X) = B X A^{- 1} = Δ_{B, A} (X)$ ; also $U (A^{1 / 2}) = (\sqrt{λ_{i}} A_{i}^{1 / 2})_{i}$ by [F6]. Apply [F2] to $U, T$ and evaluate the order inequality on $A^{1 / 2}$ in the Hilbert-Schmidt inner product. Using [F3] on both sides yields $D (A ∥ B) \leq \sum_{i} λ_{i} D (A_{i} ∥ B_{i})$ .

3.1givenF1F4step 2.1algebracases∎

For general non-negative $A_{i}, B_{i}$ , if some $D (A_{i} ∥ B_{i}) = + \infty$ , the right side is $+ \infty$ and the claim holds. Otherwise each $supp (A_{i}) \subseteq supp (B_{i})$ . If $v \in \ker B$ , where $B = \sum_{i} λ_{i} B_{i}$ , then $0 = ⟨ B v, v ⟩ = \sum_{i} λ_{i} ⟨ B_{i} v, v ⟩$ forces $B_{i} v = 0$ for every $i$ ; support inclusion then gives $A_{i} v = 0$ , so $A v = 0$ . Thus $supp (A) \subseteq supp (B)$ . Apply the positive-definite case to $A_{i} + ε I, B_{i} + ε I$ ; their weighted sums are $A + ε I, B + ε I$ . Let $ε ↓ 0$ and use [F4] for every term to obtain the desired inequality.

TheoremStatement: Literature-sourcedProof: AI-generatedOpen item page →

Finite quantum mutual information identities and the Holevo identity

Statement

For a finite-dimensional bipartite state $ρ_{A B}$ ,

$I (A : B)_{ρ} = S (ρ_{A}) + S (ρ_{B}) - S (ρ_{A B}) = D (ρ_{A B} ∥ ρ_{A} \otimes ρ_{B}) .$

For a finite classical-quantum state $ρ_{X B} = \sum_{x} p_{x} Π_{x} \otimes ρ_{x}$ , its mutual information equals its Holevo information:

$I (X : B)_{ρ} = S ⁣ (\sum_{x} p_{x} ρ_{x}) - \sum_{x : p_{x} > 0} p_{x} S (ρ_{x}) = χ ({p_{x}, ρ_{x}}) .$

Facts & Assumptions

Given: The finite-dimensional states in the Statement, with the root linear-first convention.

[F1]

Finite quantum mutual, conditional, and conditional mutual information: $I (A : B)_{ρ} = S (ρ_{A}) + S (ρ_{B}) - S (ρ_{A B})$ and $I (X : B)_{ρ} = S (ρ_{X}) + S (ρ_{B}) - S (ρ_{X B})$ .

[F2]

Finite-dimensional quantum relative entropy: on support inclusion, $D (A ∥ B) = tr (A \ln A) - tr (A \ln B)$ with support-restricted spectral logarithms.

[F3]

Joint state support is contained in the tensor product of its marginal supports: $supp (ρ_{A B}) \subseteq supp (ρ_{A} \otimes ρ_{B})$ , so the QRE in the Statement is finite.

[F4]

Finite classical-quantum states and Holevo information: $ρ_{X B} = \sum_{x} p_{x} Π_{x} \otimes ρ_{x}$ , $ρ_{B} = \sum_{x} p_{x} ρ_{x}$ , and $χ = S (ρ_{B}) - \sum_{p_{x} > 0} p_{x} S (ρ_{x})$ .

[F5]

The partial trace is characterized by the trace pairing and is basis-independent: $tr (({Tr}_{B} R) T) = tr (R (T \otimes I_{B}))$ .

[F6]

Partial trace over the first tensor factor: ${Tr}_{A}$ is the first-factor partial trace and has entries $({Tr}_{A} R)_{j j^{'}} = \sum_{i} R_{(i, j), (i, j^{'})}$ .

[F7]

Partial trace over a finite tensor factor: the second-factor partial trace has entries $({Tr}_{B} R)_{i i^{'}} = \sum_{j} R_{(i, j), (i^{'}, j)}$ .

[F8]

Ordered tensor registers, their inner product, and wire permutations: tensor product bases retain the displayed factor order and use the product inner product.

[F9]

[F10]

Finite-dimensional von Neumann entropy: entropy is $- tr (R \ln R)$ , with zero-eigenvalue terms omitted.

[F11]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln (x y) = \ln x + \ln y$ for positive $x, y$ .

Proof

1.1givenF2F3

By [F3], the support condition in [F2] holds for $ρ_{A B}$ and $ρ_{A} \otimes ρ_{B}$ , so the relative entropy is evaluated by its finite trace formula.

2.1givenF2F8F9F11step 1.1algebrachoose

Choose orthonormal eigenbases of the marginals using [F9], with positive eigenvalues $a_{i}$ for $ρ_{A}$ on its support and $b_{j}$ for $ρ_{B}$ on its support. Their product vectors form an orthonormal eigenbasis of $ρ_{A} \otimes ρ_{B}$ on its support by [F8], with eigenvalues $a_{i} b_{j} > 0$ . Since [F11] gives $\ln (a_{i} b_{j}) = \ln a_{i} + \ln b_{j}$ , spectral calculus gives $\ln (ρ_{A} \otimes ρ_{B}) = (\ln ρ_{A}) \otimes I_{B} + I_{A} \otimes (\ln ρ_{B})$ on that support.

3.1F1F2F3F5F6step 2.1algebra

Extend each marginal logarithm by zero on its kernel, which does not affect the support-restricted traces by [F2] and [F3]. Taking $T = \ln ρ_{A}$ in [F5] gives $tr (ρ_{A B} ((\ln ρ_{A}) \otimes I_{B})) = tr (ρ_{A} \ln ρ_{A})$ . For the second marginal, expanding the finite product-basis trace and using the entries in [F6] gives $tr (ρ_{A B} (I_{A} \otimes \ln ρ_{B})) = tr (ρ_{B} \ln ρ_{B})$ . Combining these identities with [F2] and step 2.1 yields $D (ρ_{A B} ∥ ρ_{A} \otimes ρ_{B}) = S (ρ_{A}) + S (ρ_{B}) - S (ρ_{A B}) = I (A : B)_{ρ}$ .

4.1givenF1F4F7F9F10F11step 2.1algebra∎

In the orthogonal blocks of $ρ_{X B}$ , the eigenvalues are $p_{x} λ_{x j}$ , where $λ_{x j}$ are the eigenvalues of $ρ_{x}$ ; zero-probability blocks contribute only zeros. By [F7] and $tr ρ_{x} = 1$ , $ρ_{X} = \sum_{x} p_{x} Π_{x}$ ; its eigenvalues are $(p_{x})$ , and the $B$ -marginal is ${\overset{ˉ}{ρ}}_{B} = \sum_{x} p_{x} ρ_{x}$ by [F4]. The block eigenvalues follow from [F9]. For $p_{x} > 0$ and $λ_{x j} > 0$ , applying [F11] and expanding $- (p_{x} λ_{x j}) \ln (p_{x} λ_{x j})$ and using $\sum_{j} λ_{x j} = 1$ gives $S (ρ_{X B}) = S (ρ_{X}) + \sum_{x : p_{x} > 0} p_{x} S (ρ_{x})$ by [F10]. Substitution into the definition [F1] cancels $S (ρ_{X})$ and proves $I (X : B)_{ρ} = χ ({p_{x}, ρ_{x}})$ .

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Partial-trace data processing for finite quantum relative entropy

Statement

Let $H_{A}, H_{B}$ be nonzero finite-dimensional complex inner-product spaces, let $d = \dim H_{B} \geq 1$ , and let $A, B$ be non-negative operators on $H_{A} \otimes H_{B}$ . Then

$D ({Tr}_{B} A ∥ {Tr}_{B} B) \leq D (A ∥ B) .$

Facts & Assumptions

Given: The spaces and non-negative operators in the Statement.

[F1]

Joint convexity of finite quantum relative entropy: QRE is jointly convex for finite convex mixtures of non-negative operators.

[F2]

Isometric invariance of finite quantum relative entropy: QRE is invariant under simultaneous isometric conjugation.

[F3]

Partial trace over a finite tensor factor: in product bases, $({Tr}_{B} R)_{i i^{'}} = \sum_{j} R_{(i, j), (i^{'}, j)}$ .

[F4]

The partial trace preserves non-negativity and total trace: the partial trace preserves non-negativity and total trace.

[F5]

Ordered tensor registers, their inner product, and wire permutations: ordered product bases and their inner products retain the stated factor order.

[F6]

Finite-dimensional quantum relative entropy: QRE uses support inclusion and the support-restricted spectral logarithms; if inclusion fails its value is $+ \infty$ .

[F7]

[F8]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

[F9]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument, so $z \mapsto ⟨ z, e_{s} ⟩ e_{r}$ is linear.

[F10]

Complex de Moivre formula for every integer exponent: for every integer $m$ and real $t$ , $(\cos t + i \sin t)^{m} = \cos (m t) + i \sin (m t)$ .

[F11]

$\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ : $\exp z = 1$ exactly when $z \in 2 π i Z$ .

[F12]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : for real $t$ , $\exp (i t) = \cos t + i \sin t$ and $∣ \exp (i t) ∣ = 1$ .

[F13]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: for positive $x, y$ , $\ln (x / y) = \ln x - \ln y$ , with $\ln 1 = 0$ .

Proof

1.1givenF3F5F8F9F10F11F12constructchoosealgebra

Choose an orthonormal basis $(e_{j})_{j < d}$ of $H_{B}$ using [F8], and set $ω = \exp (2 π i / d)$ . By [F10] and [F12], $∣ ω ∣ = 1$ and $ω^{m} = \exp (2 π i m / d)$ for every integer $m$ ; by [F11], $ω^{m} = 1$ exactly when $d$ divides $m$ . Thus $ω$ has order $d$ . Define $X e_{j} = e_{j + 1 m o d d}$ and $Z e_{j} = ω^{j} e_{j}$ ; these maps are unitary because they respectively permute the basis and multiply its vectors by unit-modulus scalars. If $d ∤ m$ , then $q = ω^{m} \neq 1$ , $q^{d} = 1$ , and $(1 - q) \sum_{b = 0}^{d - 1} q^{b} = 1 - q^{d} = 0$ , so $d^{- 1} \sum_{b = 0}^{d - 1} ω^{b m} = 0$ ; if $d ∣ m$ , that average is $1$ . Choose an orthonormal basis $(u_{i})$ of $H_{A}$ by [F8]. For $0 \leq r, s < d$ , define the linear block $R_{r s} : H_{A} \to H_{A}$ by $R_{r s} u_{i^{'}} = \sum_{i} ⟨ R (u_{i^{'}} \otimes e_{s}), u_{i} \otimes e_{r} ⟩ u_{i}$ , extending linearly. Expanding $R (u_{i^{'}} \otimes e_{s})$ in the product basis [F5] then gives $R = \sum_{r, s} R_{r s} \otimes M_{r s}$ , where $M_{r s} z : = ⟨ z, e_{s} ⟩ e_{r}$ : both sides agree on every product basis vector. Direct application to basis vectors gives $Z^{b} M_{r s} (Z^{b})^{*} = ω^{b (r - s)} M_{r s}$ and $X^{a} M_{r s} (X^{a})^{*} = M_{r + a, s + a}$ , with indices modulo $d$ . For $0 \leq r, s < d$ , $d ∣ (r - s)$ exactly when $r = s$ , so the proved phase average removes precisely the off-diagonal units. Also $d^{- 1} \sum_{a = 0}^{d - 1} M_{r + a, r + a} = I_{B} / d$ . Therefore $T (R) : = d^{- 2} \sum_{a, b} (I_{A} \otimes X^{a} Z^{b}) R (I_{A} \otimes X^{a} Z^{b})^{*} = \sum_{r} R_{r r} \otimes I_{B} / d = {Tr}_{B} (R) \otimes I_{B} / d$ by [F3]. For every $a, b$ , the lifted map $I_{A} \otimes X^{a} Z^{b}$ sends $u_{i} \otimes e_{j}$ to $ω^{b j} u_{i} \otimes e_{j + a}$ , hence sends an orthonormal product basis to an orthonormal product basis; it is therefore unitary, including $d = 1$ . When $d = 1$ , $X = Z = I_{B}$ and there is only the diagonal unit, so the same formula holds directly.

1.2givenF6F7F13algebra

For non-negative $C, D$ on $H_{A}$ , their tensor products with $I_{B} / d$ have supports $supp (C) \otimes H_{B}$ and $supp (D) \otimes H_{B}$ by the tensor-product eigenbases [F7]. Thus support inclusion holds for $(C, D)$ exactly when it holds for $(C \otimes I_{B} / d, D \otimes I_{B} / d)$ . In the finite branch, each positive tensor eigenvalue has the form $λ / d$ , and [F13] gives $\ln (λ / d) = \ln λ - \ln d$ ; the two logarithms therefore have the same additive term $- \ln d$ , which cancels, while $tr (I_{B} / d) = 1$ ; hence $D (C \otimes I_{B} / d ∥ D \otimes I_{B} / d) = D (C ∥ D)$ . If inclusion fails both sides are $+ \infty$ by [F6].

2.1givenF1F2step 1.1algebra

Apply joint convexity [F1] to the finite average defining $T$ and isometric invariance [F2] to each unitary conjugate. This gives $D (T (A) ∥ T (B)) \leq D (A ∥ B)$ .

3.1givenF4step 1.1step 1.2step 2.1algebra∎

By [F4], $C = {Tr}_{B} A$ and $D = {Tr}_{B} B$ are non-negative. Substitute them into step 1.2, use step 1.1 to identify their twirls, and then apply step 2.1 to obtain $D ({Tr}_{B} A ∥ {Tr}_{B} B) \leq D (A ∥ B)$ .

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Channel data processing for finite quantum relative entropy

Statement

Let $H, K$ be nonzero finite-dimensional complex inner-product spaces, let $Φ : L (H) \to L (K)$ be a quantum channel (Finite-dimensional quantum channel), and let $A, B$ be non-negative operators on $H$ . Then

$D (Φ (A) ∥ Φ (B)) \leq D (A ∥ B) .$

Facts & Assumptions

Given: The spaces, channel and non-negative operators in the Statement.

[F1]

Kraus and Choi characterizations of complete positivity: a finite-dimensional completely positive map has a finite Kraus representation.

[F2]

Finite Kraus representation: a Kraus representation has the form $Φ (X) = \sum_{j} K_{j} X K_{j}^{*}$ on the full operator space.

[F3]

Trace preservation is Kraus normalization: trace preservation is equivalent to $\sum_{j} K_{j}^{*} K_{j} = I_{H}$ .

[F4]

Partial-trace data processing for finite quantum relative entropy: partial trace over a nonzero finite factor does not increase QRE.

[F5]

Isometric invariance of finite quantum relative entropy: simultaneous isometric conjugation preserves QRE.

[F6]

Partial trace over a finite tensor factor: partial trace over the environment removes the matching diagonal Kraus blocks and retains the output operator.

[F7]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ K x, K y ⟩ = ⟨ x, K^{*} K y ⟩$ under the repository's inner-product convention.

[F8]

Finite registers and their ordered computational bases: the standard register $E = C^{r}$ has the specified ordered orthonormal basis $(f_{j})$ .

Proof

1.1givenF1F2F3F7F8construct

By [F1]–[F2], choose a finite Kraus family $(K_{j})_{j < r}$ for $Φ$ . Since $H \neq {0}$ and [F3] gives $\sum_{j} K_{j}^{*} K_{j} = I_{H}$ , the family is nonempty. Let $E = C^{r}$ with the ordered orthonormal basis $(f_{j})$ from [F8], and define $V : H \to K \otimes E$ by $V x : = \sum_{j < r} K_{j} x \otimes f_{j}$ . For $x, y \in H$ , orthonormality and [F3], [F7] give $⟨ V x, V y ⟩ = \sum_{j} ⟨ K_{j} x, K_{j} y ⟩ = ⟨ x, (\sum_{j} K_{j}^{*} K_{j}) y ⟩ = ⟨ x, y ⟩$ ; hence $V^{*} V = I_{H}$ .

2.1givenF2F6F8step 1.1algebra

Expanding in the environment basis [F8] gives $V X V^{*} = \sum_{j, k} K_{j} X K_{k}^{*} \otimes M_{j k}$ , where $M_{j k} z = ⟨ z, f_{k} ⟩ f_{j}$ . The partial-trace formula [F6] keeps exactly the terms $j = k$ , so ${Tr}_{E} (V X V^{*}) = \sum_{j} K_{j} X K_{j}^{*} = Φ (X)$ for every $X$ .

3.1givenF4F5step 2.1algebra∎

Apply isometric invariance [F5] and then partial-trace data processing [F4] to the pair $(V A V^{*}, V B V^{*})$ on $K \otimes E$ . By step 2.1, $D (Φ (A) ∥ Φ (B)) = D ({Tr}_{E} (V A V^{*}) ∥ {Tr}_{E} (V B V^{*})) \leq D (V A V^{*} ∥ V B V^{*}) = D (A ∥ B)$ .

Remarks

The finite Stinespring dilation used in the proof is summarized by the following map diagram. It records the factor that is discarded by the partial trace; the proof relies on the Kraus and trace calculations above, not on the diagram.

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Nonnegativity and equality for finite quantum relative entropy

Statement

For density operators $ρ, σ$ on a finite-dimensional complex inner-product space,

$D (ρ ∥ σ) \geq 0,$

with equality if and only if $ρ = σ$ .

Facts & Assumptions

Given: The states $ρ, σ$ in the Statement.

[F1]

Channel data processing for finite quantum relative entropy: applying one quantum channel to both arguments cannot increase QRE.

[F2]

A finite POVM defines a classical-output quantum channel: every finite POVM gives a channel to a diagonal classical register with its stated outcome weights.

[F3]

Nonnegativity and equality for finite classical relative entropy: finite classical relative entropy is non-negative and vanishes exactly for equal probability vectors.

[F4]

Finite POVMs and their outcome law: a finite POVM is a non-negative operator family summing to the identity, and its state outcome weights are $tr (ρ E_{y})$ .

[F5]

POVM outcome weights are probabilities: finite POVM weights of a density operator form a probability vector.

[F6]

Non-negative and positive operators: non-negative means self-adjoint with nonnegative quadratic form.

[F7]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

[F8]

Density operator: states are non-negative operators of trace one.

[F9]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument and conjugate-symmetric.

[F10]

Finite-dimensional quantum relative entropy: if support inclusion holds, $D (A ∥ B) = tr (A \ln A) - tr (A \ln B)$ .

[F11]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln 1 = 0$ .

Proof

1.1givenF1F2F4F5F8F10F11algebra

The singleton POVM $E_{0} = I_{H}$ is a finite POVM by [F4]. By [F8] the inputs have trace one, and [F2] sends each density operator to the scalar state $1$ on a one-dimensional register. The definition [F10] and $\ln 1 = 0$ from [F11] give $D (1 ∥ 1) = 0$ , so applying [F1] yields $D (ρ ∥ σ) \geq 0$ .

1.2givenF1F3F4F5F6F7F9construct

Suppose $D (ρ ∥ σ) = 0$ and choose any orthonormal basis $(e_{j})_{j < d}$ of $H$ using [F7]. The rank-one maps $P_{j} x : = ⟨ x, e_{j} ⟩ e_{j}$ are self-adjoint and satisfy $⟨ P_{j} x, x ⟩ = ∣ ⟨ x, e_{j} ⟩ ∣^{2} \geq 0$ by [F9], so they are non-negative by [F6]. Their sum is $I_{H}$ , so [F4] makes them a finite POVM; it has nonempty outcome set because $H \neq {0}$ . By [F5], the outcome vectors $p_{j} = tr (ρ P_{j})$ and $q_{j} = tr (σ P_{j})$ are probability vectors. Data processing [F1] and classical KL nonnegativity [F3] give $0 = D (ρ ∥ σ) \geq D (p ∥ q) \geq 0$ , so $p_{j} = q_{j}$ for every $j$ .

2.1givenF6F7F9step 1.2algebrachoose

For any unit vector $v \in H$ , extend $v$ to an orthonormal basis using [F7]. Step 1.2 applied to that basis gives $⟨ ρ v, v ⟩ = ⟨ σ v, v ⟩$ ; by homogeneity this equality holds for every $v$ . Put $Δ = ρ - σ$ , which is self-adjoint by [F6], and $q (v) = ⟨ Δ v, v ⟩$ . Under the root convention [F9], expansion gives $4 ⟨ Δ x, y ⟩ = q (x + y) - q (x - y) + i q (x + i y) - i q (x - i y)$ . Since every $q (v) = 0$ , all matrix coefficients of $Δ$ vanish, hence $ρ = σ$ .

3.1givenF10algebra∎

Conversely, if $ρ = σ$ , [F10] gives the support inclusion, and the two spectral logarithmic traces in the QRE definition agree, so $D (ρ ∥ σ) = 0$ .

TheoremStatement: Literature-sourcedProof: AI-generatedOpen item page →

The finite Holevo measurement bound

Statement

Let $X$ be a finite nonempty set, let $(p_{x})$ be a probability vector, let $ρ_{x}$ be density operators on a nonzero finite-dimensional space $H_{B}$ , and let $\overset{ˉ}{ρ} : = \sum_{x} p_{x} ρ_{x}$ . For a finite POVM $(E_{y})_{y \in Y}$ on $H_{B}$ , define $w (y ∣ x) : = tr (ρ_{x} E_{y})$ , $q_{y} : = \sum_{x} p_{x} w (y ∣ x)$ , and the classical mutual information

$I (X : Y) : = \sum_{x, y : p_{x} w (y ∣ x) > 0} p_{x} w (y ∣ x) \ln \frac{w (y ∣ x)}{q_{y}} .$

Then

$I (X : Y) \leq χ ({p_{x}, ρ_{x}}) = S (\overset{ˉ}{ρ}) - \sum_{x : p_{x} > 0} p_{x} S (ρ_{x}) .$

Facts & Assumptions

Given: The finite ensemble, average state, POVM, and outcome probabilities in the Statement.

[F1]

Finite classical-quantum states and Holevo information: $χ = S (\overset{ˉ}{ρ}) - \sum_{p_{x} > 0} p_{x} S (ρ_{x})$ for the associated cq state.

[F2]

Finite-dimensional quantum relative entropy: QRE is computed by the support-restricted spectral logarithm, with $+ \infty$ when supports fail.

[F3]

Channel data processing for finite quantum relative entropy: QRE cannot increase under a finite-dimensional quantum channel.

[F4]

A finite POVM defines a classical-output quantum channel: the POVM defines a channel whose output on a state has diagonal entries $tr (ρ E_{y})$ .

[F5]

POVM outcome weights are probabilities: each $w (\cdot ∣ x)$ is a probability vector.

[F6]

[F7]

Trace is a linear functional on $M_{n} (F)$ : trace is linear over finite sums and scalar multiples.

Proof

1.1givenF2F6algebra

Fix $x$ with $p_{x} > 0$ . The operator $\overset{ˉ}{ρ} - p_{x} ρ_{x} = \sum_{z \neq x} p_{z} ρ_{z}$ is non-negative. If $v \in \ker \overset{ˉ}{ρ}$ , then $0 = ⟨ \overset{ˉ}{ρ} v, v ⟩ \geq p_{x} ⟨ ρ_{x} v, v ⟩ \geq 0$ , so [F6] gives $ρ_{x} v = 0$ . Thus $\ker \overset{ˉ}{ρ} \subseteq \ker ρ_{x}$ and $supp (ρ_{x}) \subseteq supp (\overset{ˉ}{ρ})$ ; $D (ρ_{x} ∥ \overset{ˉ}{ρ})$ is finite for every $x$ with $p_{x} > 0$ .

2.1givenF2F3F4F5F7step 1.1algebra

The measurement channel [F4] sends $ρ_{x}$ to the diagonal state with entries $w (y ∣ x)$ and $\overset{ˉ}{ρ}$ to the diagonal state with entries $q_{y}$ by linearity [F7]. For $p_{x} > 0$ , if $w (y ∣ x) > 0$ then $q_{y} \geq p_{x} w (y ∣ x) > 0$ . The QRE formula [F2] on diagonal states and data processing [F3] therefore give $D (ρ_{x} ∥ \overset{ˉ}{ρ}) \geq \sum_{y : w (y ∣ x) > 0} w (y ∣ x) \ln \frac{w (y ∣ x)}{q_{y}}$ .

3.1givenF1F2F7step 1.1step 2.1algebra∎

Multiply step 2.1 by $p_{x}$ and sum only over $x$ with $p_{x} > 0$ . Extend the support logarithm of $\overset{ˉ}{ρ}$ by zero on its kernel; step 1.1 and [F2] ensure that this preserves every retained cross trace. Trace linearity [F7] and $\overset{ˉ}{ρ} = \sum_{x : p_{x} > 0} p_{x} ρ_{x}$ give $\sum_{x : p_{x} > 0} p_{x} D (ρ_{x} ∥ \overset{ˉ}{ρ}) = \sum_{x : p_{x} > 0} p_{x} tr (ρ_{x} \ln ρ_{x}) - tr (\overset{ˉ}{ρ} \ln \overset{ˉ}{ρ}) = χ$ by [F1]. The summed measurement terms are exactly the displayed $I (X : Y)$ by its definition. Hence $I (X : Y) \leq χ$ .

5 · Examples, counterexamples and false statements

None yet.