PropositionStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Trace Holder Inequality

Statement

For finite-dimensional complex inner-product spaces $H, K$ and compatible linear maps $A, B : H \to K$ (Linear map between vector spaces over the same field), the composite $B^{*} A$ is an endomorphism of $H$ and

$∣ {tr}_{H} (B^{*} A) ∣ \leq ∥ A ∥_{1} ∥ B ∥ .$

Facts & Assumptions

Given: The finite-dimensional spaces and maps in the Statement.

[F1]

Trace-norm duality says $∥ A ∥_{1} = \max_{∥ C ∥ \leq 1} ∣ {tr}_{H} (C^{*} A) ∣$ (Trace Norm Duality And Norm Properties).

[F2]

The operator norm is $0$ when $H = 0$ and otherwise is defined as the maximum of $∥ B v ∥$ over unit vectors (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

[F3]

For real $β$ , $(β^{- 1} B)^{*} = β^{- 1} B^{*}$ when $β > 0$ , and $0^{*} = 0$ (Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ ).

[F4]

The trace is computed by diagonal sums in any ordered basis and vanishes on the zero space (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[F5]

The root inner product is linear in its first argument, and the induced length satisfies $∥ v ∥^{2} = ⟨ v, v ⟩$ (Real and complex inner-product spaces and their induced length).

[F6]

Complex modulus is nonnegative and multiplicative (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F7]

An SVD expresses $B$ using its positive singular values and orthonormal domain and codomain vectors (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).

[F8]

For an orthonormal basis, the sum of the squared coordinate moduli equals the squared vector length, including the empty-basis case (Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis).

[F9]

In an ordered basis, the $j$ -th matrix column of an endomorphism is the coordinate column of its image on the $j$ -th basis vector (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

Proof

1.1givenF2F3F4F7F8algebra

Put $β = ∥ B ∥$ . If $H = 0$ , [F2] defines $β = 0$ . If $H \neq 0$ , choose an SVD of $B$ from [F7], with positive singular values $t_{1} \geq \dots \geq t_{q} > 0$ and orthonormal domain vectors $(u_{j})$ . If $q > 0$ , [F8] gives $∥ B v ∥^{2} = \sum_{j \leq q} t_{j}^{2} ∣ ⟨ v, u_{j} ⟩ ∣^{2} \leq t_{1}^{2}$ for every unit vector $v$ , with equality at $u_{1}$ . If $q = 0$ , the SVD gives $B = 0$ , and every unit vector attains $0$ . Thus the maximum in [F2] exists in all cases. When $β = 0$ , every unit vector has $B v = 0$ ; scaling and linearity give $B = 0$ (also when $H = 0$ ). By [F3], $B^{*} = 0$ , and then $B^{*} A = 0$ , whose trace is $0$ by [F4]; both sides of the inequality are $0$ .

2.1F1F2F5step 1.1algebra

Suppose $β > 0$ and put $C = B / β$ . For every unit vector $v$ , $∥ C v ∥^{2} = ⟨ β^{- 1} B v, β^{- 1} B v ⟩ = β^{- 2} ∥ B v ∥^{2},$ so nonnegativity gives $∥ C v ∥ = ∥ B v ∥ / β \leq 1$ by [F2]. Applying the argument in step 1.1 with $C$ in place of $B$ shows its defining maximum exists and is at most $1$ , hence $∥ C ∥ \leq 1$ . Trace-norm duality [F1] gives $∣ {tr}_{H} (C^{*} A) ∣ \leq ∥ A ∥_{1}$ .

3.1F3F4F6F9step 2.1algebra∎

Since $β$ is a positive real, [F3] gives $C^{*} = β^{- 1} B^{*}$ . Fix an ordered basis of $H$ . The coordinate column of $β^{- 1} (B^{*} A) e_{j}$ is $β^{- 1}$ times the coordinate column of $(B^{*} A) e_{j}$ , by uniqueness of coordinates and [F9]; hence their diagonal entries have the same scaling. Summing them by [F4] gives ${tr}_{H} (C^{*} A) = β^{- 1} {tr}_{H} (B^{*} A)$ . Thus step 2.1 and modulus homogeneity [F6] yield $β^{- 1} ∣ {tr}_{H} (B^{*} A) ∣ \leq ∥ A ∥_{1}$ . Multiplying by $β$ proves the inequality when $β > 0$ ; step 1.1 proves the $β = 0$ case.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information (2018 author-hosted draft), Chapter 1, §1.1.3, Eq. (1.174) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27), Appendices A.5 and A.7 (standard reference, not scraped)