Broadcasting: the BCFJS theorem, states can be broadcast iff they commute

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Row BC of specs/BACKLOG.md (the BCFJS iff of Empirical/QM/NoBroadcasting.lean), milestones BC1–BC6: complete.

A channel Φ : ℂⁿ → ℂⁿ ⊗ ℂⁿ broadcasts ρ when both marginals of Φ ρ are ρ (Channel.Broadcasts). Barnum–Caves–Fuchs–Jozsa–Schumacher (1996): a pair of states can be broadcast by one channel iff they commute. This file proves both halves: the constructive half by the classical copier in a joint eigenbasis, and the hard half by an elementary route through support confinement (no fidelity, no relative entropy), assembled by induction on rank.

• Channel.Broadcasts, with Broadcasts.add, .smul, .sub — the condition is linear in the state, so a broadcaster of two states broadcasts their whole span;
• Matrix.PosSemidef.mul_mul_conjTranspose_eq_zero_iff, Matrix.PosSemidef.eq_zero_of_sum_eq_zero — the two positive-semidefinite squeezes the argument uses;
• ★ Channel.Broadcasts.kronecker_mul_kraus_mul — support confinement: if Φ broadcasts the positive semidefinite ρ and P is a projector with P ρ = ρ, every Kraus operator maps the range of ρ into range P ⊗ range P, (P ⊗ P) Kᵢ ρ = Kᵢ ρ (the compressed output (Q ⊗ 1) Φ(ρ) (Q ⊗ 1) has trace Tr(ρ Q) = 0, so it and each Kraus term vanish);
• onbVec, onbProj, sum_onbProj — an orthonormal basis of ℂⁿ as coordinate vectors, its rank-one projectors, and completeness; copierKraus, copierChannel — the classical copier X ↦ ∑ₖ ⟨b k|X|b k⟩ · |b k b k⟩⟨b k b k|, a channel; ★ copierChannel_broadcasts — it broadcasts every matrix diagonal in its basis;
• ★ exists_orthonormalBasis_mulVec_eq_smul_of_commute — two commuting Hermitian matrices have a joint orthonormal eigenbasis (Mathlib's joint eigenspace decomposition LinearMap.IsSymmetric.directSum_isInternal_of_commute, restricted to the finitely many eigenvalue pairs and collected into a basis);
• ★★ exists_channel_broadcasts_of_commute — commuting Hermitian matrices can be broadcast (BC1, the easy half of BCFJS);
• ★★ Channel.Broadcasts.star_dotProduct_eq_zero_or_norm_eq_one — two broadcast pure states are orthogonal or parallel (BC2): a broadcast pure state is cloned (Broadcasts.kraus_mulVec_eq_smul_kronVec, from support confinement with the rank-one projector), and trace preservation read on the two vectors (Channel.star_dotProduct_eq_sum_kraus) gives ⟨φ|ψ⟩ = ⟨φ|ψ⟩² ∑ᵢ conj bᵢ aᵢ with |∑ᵢ conj bᵢ aᵢ| ≤ 1 by Cauchy–Schwarz (norm_star_dotProduct_sq_le). This is the no-cloning theorem at channel level, and the rank-one case of the hard half;
• suppProj A — the support projector, the orthogonal projector onto the range of A (Submodule.starProjection read as a matrix): Hermitian, idempotent, suppProj A * A = A, and suppProj A x = x ↔ x ∈ range A (suppProj_mulVec_eq_self_iff);
• nsq (the squared norm Re ⟨v|v⟩), IsHermitian.exists_top_eigenvalue — the top eigenvalue of a Hermitian matrix bounds its Rayleigh quotient and is attained by a unit eigenvector; nsq_proj_mulVec_le, proj_mulVec_eq_self_of_nsq_eq — a projector contracts, with equality only on its range; re_star_dotProduct_kronecker_mulVec_le — the tensor bound ⟨x|Q ⊗ Q|x⟩ ≤ μ² ‖x‖² from ⟨z|Q|z⟩ ≤ μ ‖z‖², through the identity μ² − Q ⊗ Q = μ (μ − Q) ⊗ 1 + Q ⊗ (μ − Q);
• ★★ Channel.Broadcasts.mul_eq_zero_of_range_disjoint — BC3: broadcast states with disjoint supports have orthogonal supports, B A = 0. With Q = P_A P_B P_A and its top eigenvalue μ, attained at u ∈ range A, and w = P_B u ∈ range B: μ = ⟨w|u⟩ = ∑ᵢ ⟨Kᵢ w|Kᵢ u⟩, each term is ⟨Kᵢ w|(G ⊗ G) Kᵢ u⟩ by confinement, the tensor bound and Cauchy–Schwarz give μ ≤ μ √μ, so μ ∈ {0, 1}; μ = 1 would put u in both ranges. BC2 is the rank-one case;
• Matrix.PosSemidef.mul_eq_zero_of_trace_mul_eq_zero (two positive semidefinite matrices with Tr (X Y) = 0 have X Y = 0), Channel.star_dotProduct_adjoint_mulVec (⟨v|Φ† P|v⟩ = ∑ᵢ ⟨Kᵢ v|P|Kᵢ v⟩), Channel.adjoint_kronecker_one_mulVec_eq_self (the dual of P ⊗ 1 fixes a vector whose Kraus images lie in range P ⊗ ℂⁿ), and the partial-trace identity traceRight_kronecker_mul_mul_kronecker, Tr_B ((A ⊗ B) Y (C ⊗ D)) = A · Tr_B (Y (1 ⊗ D B)) · C (with its traceLeft twin);
• ★ Channel.Broadcasts.kronecker_mulVec_kraus_mulVec_sub — BC4 (i): if Φ broadcasts the positive semidefinite τ and every Kraus operator maps a subspace V ⊆ supp τ into V ⊗ V, then it maps W = supp τ ⊖ V into W ⊗ W: the dual Φ† (P_V ⊗ 1) fixes V, so its excess over P_V is positive semidefinite with zero trace against τ and kills the support;
• ★★ Channel.Broadcasts.block_split — BC4: a cloned subspace splits a broadcast state into blocks, each broadcast: P_V τ P_W = 0, and Φ broadcasts P_V τ P_V and P_W τ P_W. The cross blocks Φ (P_V τ P_W) are sandwiched between P_V ⊗ P_V and P_W ⊗ P_W (kraus_block_sandwich), whose partial traces vanish because P_W P_V = 0;
• onbProjSet (the projector onto the span of a subfamily of an orthonormal basis, with onbProjSet_mul_self and star_dotProduct_onbProjSet_mulVec), nsq_eq_sum_onb (Parseval), re_star_dotProduct_mulVec_eq_sum_onb (the Rayleigh quotient of a diagonalised matrix);
• ★★ exists_boundary_point — BC5: the segment through two distinct states meets the boundary of the cone: for positive semidefinite ρ ≠ σ of trace one there is l ≥ 1 with σ + l (ρ − σ) positive semidefinite and a kernel vector outside ker (ρ + σ). The admissible l form a closed bounded set (the traceless ρ − σ has a negative direction); at its supremum, a missing kernel vector would let the eigenvalue-0 eigenvectors (which lie in ker (ρ + σ), hence in ker (ρ − σ)) and the positive eigenvalues absorb a further step δ = ε / (μ + 1), contradicting maximality;
• suppProj_mulVec_eq_zero_iff (the support projector of a Hermitian matrix vanishes exactly on its kernel), Matrix.PosSemidef.add_mulVec_eq_zero_iff (a positive combination of positive semidefinite matrices vanishes on x iff both do), rank_lt_rank_of_ker (a strict kernel inclusion is a strict rank inequality, by rank–nullity); interProj P₁ P₂ — the projector onto the intersection of two ranges, 1 − suppProj ((1 − P₁) + (1 − P₂)), with interProj_mulVec_eq_self_iff and mul_interProj; interProj_kronecker_mulVec_eq_self — intersections of tensor squares: a vector in S₁ ⊗ S₁ and in S₂ ⊗ S₂ lies in (S₁ ∩ S₂) ⊗ (S₁ ∩ S₂) (column by column, row by row);
• ★★★ Channel.Broadcasts.mul_comm_of_posSemidef — BC6, the hard half of BCFJS: broadcast states commute. Strong induction on rank (ρ + σ): normalise to trace one (Matrix.PosSemidef.exists_smul_trace_one); take the two boundary points τ₁, τ₂ of the segment (BC5), broadcast by linearity, with [τ₁, τ₂] = (l₁ + l₂ − 1) [ρ, σ]; with V the intersection of their supports, either V = 0 and BC3 gives τ₁ τ₂ = 0 = τ₂ τ₁, or V ≠ 0 is cloned by every Kraus operator, BC4 splits each τᵢ into a V-block and a complementary block, the two pairs of blocks are broadcast with strictly smaller rank of their sum (witnessed by the BC5 kernel vector and by a vector of V), so they commute by induction, and the cross products vanish;
• ★★★ exists_channel_broadcasts_iff_commute — BCFJS: two positive semidefinite matrices can be broadcast by a single channel iff they commute (BC1 and BC6);
• exists_orthonormalBasis_mulVec_eq_smul_of_pairwise_commute (a pairwise-commuting family of Hermitian matrices has a joint orthonormal eigenbasis), ★★ exists_channel_broadcasts_of_pairwise_commute, and ★★★ exists_channel_broadcasts_family_iff_pairwise_commute — BCFJS for finite families: a finite family of positive semidefinite matrices can be broadcast by a single channel iff its members pairwise commute (the copier in a joint eigenbasis one way, the pair theorem applied pairwise the other).

Provenance

The literature proves the hard half through fidelity monotonicity (BCFJS 1996) or the equality case of the relative-entropy data-processing inequality (Lindblad 1999). Neither is in Mathlib or in this corpus, and neither is used here: the route above needs only support confinement, trace preservation and elementary matrix analysis. Row BC of specs/BACKLOG.md records the milestones BC1–BC6, and specs/bcfjs-note.md states the argument in prose, step by step, with the upstream question asked at the pin.

Source

Barnum, Caves, Fuchs, Jozsa, Schumacher, Phys. Rev. Lett. 76, 2818 (1996).

theorem Matrix.traceLeft_one_kronecker_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq m] (X : Matrix n n R) (M : Matrix (m × n) (m × n) R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 X * M).traceLeft = X * M.traceLeft

Partial trace over the first factor is a left module map over I ⊗ X. traceLeft ((I ⊗ₖ X) · M) = X · traceLeft M.

theorem Matrix.traceLeft_mul_one_kronecker {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq m] (M : Matrix (m × n) (m × n) R) (X : Matrix n n R) : (M * kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 X).traceLeft = M.traceLeft * X

Partial trace over the first factor is a right module map over I ⊗ X. traceLeft (M · (I ⊗ₖ X)) = traceLeft M · X.

def QuantumInfo.Channel.Broadcasts {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] (Φ : Channel n (n × n) ι) (ρ : Matrix n n ℂ) : Prop

A channel Φ : ℂⁿ → ℂⁿ ⊗ ℂⁿ broadcasts ρ when both marginals of Φ ρ are ρ.

Equations

• Φ.Broadcasts ρ = ((Φ.apply ρ).traceRight = ρ ∧ (Φ.apply ρ).traceLeft = ρ)

theorem QuantumInfo.Channel.Broadcasts.add {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ σ : Matrix n n ℂ} (hρ : Φ.Broadcasts ρ) (hσ : Φ.Broadcasts σ) : Φ.Broadcasts (ρ + σ)

theorem QuantumInfo.Channel.Broadcasts.smul {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ : Matrix n n ℂ} (hρ : Φ.Broadcasts ρ) (c : ℂ) : Φ.Broadcasts (c • ρ)

theorem QuantumInfo.Channel.Broadcasts.sub {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ σ : Matrix n n ℂ} (hρ : Φ.Broadcasts ρ) (hσ : Φ.Broadcasts σ) : Φ.Broadcasts (ρ - σ)

theorem Matrix.PosSemidef.mul_mul_conjTranspose_eq_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_3} {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (L : Matrix m n ℂ) : L * ρ * L.conjTranspose = 0 ↔ L * ρ = 0

For ρ positive semidefinite, L ρ Lᴴ = 0 forces L ρ = 0: write ρ = Bᴴ B, so L ρ Lᴴ = (L Bᴴ)(L Bᴴ)ᴴ.

theorem Matrix.PosSemidef.eq_zero_of_sum_eq_zero {ι : Type u_2} [Fintype ι] {m : Type u_3} [Fintype m] {T : ι → Matrix m m ℂ} (hT : ∀ (i : ι), (T i).PosSemidef) (h : ∑ i : ι, T i = 0) (i : ι) : T i = 0

A finite sum of positive semidefinite matrices that vanishes has every term zero.

theorem QuantumInfo.Channel.Broadcasts.kronecker_one_mul_kraus_mul {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ : Matrix n n ℂ} (h : Φ.Broadcasts ρ) (hρ : ρ.PosSemidef) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (hPρ : P * ρ = ρ) (i : ι) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1 * (Φ.kraus i * ρ) = Φ.kraus i * ρ

Support confinement, first factor. If Φ broadcasts the positive semidefinite ρ and P is a projector with P ρ = ρ, then every Kraus operator maps the range of ρ into range P ⊗ ℂⁿ: (P ⊗ 1) Kᵢ ρ = Kᵢ ρ.

theorem QuantumInfo.Channel.Broadcasts.one_kronecker_mul_kraus_mul {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ : Matrix n n ℂ} (h : Φ.Broadcasts ρ) (hρ : ρ.PosSemidef) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (hPρ : P * ρ = ρ) (i : ι) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P * (Φ.kraus i * ρ) = Φ.kraus i * ρ

Support confinement, second factor: (1 ⊗ P) Kᵢ ρ = Kᵢ ρ.

theorem QuantumInfo.Channel.Broadcasts.kronecker_mul_kraus_mul {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ρ : Matrix n n ℂ} (h : Φ.Broadcasts ρ) (hρ : ρ.PosSemidef) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (hPρ : P * ρ = ρ) (i : ι) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P P * (Φ.kraus i * ρ) = Φ.kraus i * ρ

Support confinement. If Φ broadcasts the positive semidefinite ρ and P is a projector with P ρ = ρ, every Kraus operator maps the range of ρ into range P ⊗ range P: (P ⊗ P) Kᵢ ρ = Kᵢ ρ.

Commuting states are broadcastable: the classical copier in a joint eigenbasis

noncomputable def QuantumInfo.onbVec {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : n → ℂ

The coordinate vector of b k.

Equations

• QuantumInfo.onbVec b k = (b k).ofLp

theorem QuantumInfo.star_onbVec_dotProduct {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k l : n) : star (onbVec b k) ⬝ᵥ onbVec b l = if k = l then 1 else 0

theorem QuantumInfo.star_onbVec_dotProduct_self {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : star (onbVec b k) ⬝ᵥ onbVec b k = 1

noncomputable def QuantumInfo.onbProj {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : Matrix n n ℂ

The rank-one projector |b k⟩⟨b k|.

Equations

• QuantumInfo.onbProj b k = Matrix.vecMulVec (QuantumInfo.onbVec b k) (star (QuantumInfo.onbVec b k))

theorem QuantumInfo.sum_onbProj {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) : ∑ k : n, onbProj b k = 1

Completeness: ∑ₖ |b k⟩⟨b k| = 1.

noncomputable def QuantumInfo.copierKraus {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : Matrix (n × n) n ℂ

The Kraus operator |b k ⊗ b k⟩⟨b k| of the copier.

Equations

• QuantumInfo.copierKraus b k = Matrix.vecMulVec (fun (p : n × n) => QuantumInfo.onbVec b k p.1 * QuantumInfo.onbVec b k p.2) (star (QuantumInfo.onbVec b k))

theorem QuantumInfo.copierKraus_conjTranspose_mul {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : (copierKraus b k).conjTranspose * copierKraus b k = onbProj b k

noncomputable def QuantumInfo.copierChannel {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) : Channel n (n × n) n

The copier channel of an orthonormal basis: X ↦ ∑ₖ ⟨b k| X |b k⟩ · |b k b k⟩⟨b k b k|.

Equations

• QuantumInfo.copierChannel b = { kraus := QuantumInfo.copierKraus b, tp := ⋯ }

theorem QuantumInfo.copierChannel_kraus {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) : (copierChannel b).kraus k = copierKraus b k

theorem QuantumInfo.copierKraus_mul_mul_conjTranspose {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (ρ : Matrix n n ℂ) (k : n) : copierKraus b k * ρ * (copierKraus b k).conjTranspose = (star (onbVec b k) ⬝ᵥ ρ.mulVec (onbVec b k)) • Matrix.vecMulVec (fun (p : n × n) => onbVec b k p.1 * onbVec b k p.2) (star fun (p : n × n) => onbVec b k p.1 * onbVec b k p.2)

The copier on a rank-one term: Kₖ ρ Kₖᴴ = ⟨b k|ρ|b k⟩ • |b k b k⟩⟨b k b k|.

theorem QuantumInfo.traceRight_kron_vecMulVec {n : Type u_1} [Fintype n] (v : n → ℂ) (hv : star v ⬝ᵥ v = 1) : (Matrix.vecMulVec (fun (p : n × n) => v p.1 * v p.2) (star fun (p : n × n) => v p.1 * v p.2)).traceRight = Matrix.vecMulVec v (star v)

theorem QuantumInfo.traceLeft_kron_vecMulVec {n : Type u_1} [Fintype n] (v : n → ℂ) (hv : star v ⬝ᵥ v = 1) : (Matrix.vecMulVec (fun (p : n × n) => v p.1 * v p.2) (star fun (p : n × n) => v p.1 * v p.2)).traceLeft = Matrix.vecMulVec v (star v)

theorem QuantumInfo.eq_sum_smul_onbProj {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) {ρ : Matrix n n ℂ} {r : n → ℂ} (hdiag : ∀ (k : n), ρ.mulVec (onbVec b k) = r k • onbVec b k) : ρ = ∑ k : n, r k • onbProj b k

A matrix diagonal in the basis b is the sum of its eigenvalues times the projectors.

theorem QuantumInfo.copierChannel_broadcasts {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) {ρ : Matrix n n ℂ} {r : n → ℂ} (hdiag : ∀ (k : n), ρ.mulVec (onbVec b k) = r k • onbVec b k) : (copierChannel b).Broadcasts ρ

★ The copier broadcasts every matrix diagonal in its basis.

Joint eigenbasis of commuting Hermitian matrices

theorem QuantumInfo.exists_orthonormalBasis_mulVec_eq_smul_of_commute {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (hc : ρ * σ = σ * ρ) : ∃ (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (r : n → ℂ) (s : n → ℂ), (∀ (k : n), ρ.mulVec (onbVec b k) = r k • onbVec b k) ∧ ∀ (k : n), σ.mulVec (onbVec b k) = s k • onbVec b k

Two commuting Hermitian matrices have a joint orthonormal eigenbasis (Mathlib's LinearMap.IsSymmetric.directSum_isInternal_of_commute, read through Matrix.toEuclideanLin).

theorem QuantumInfo.exists_channel_broadcasts_of_commute {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (hc : ρ * σ = σ * ρ) : ∃ (Φ : Channel n (n × n) n), Φ.Broadcasts ρ ∧ Φ.Broadcasts σ

★★ Commuting Hermitian matrices can be broadcast: the copier in a joint eigenbasis broadcasts both (the easy half of BCFJS).

Broadcasting two pure states forces them orthogonal or parallel (the cloning core)

def QuantumInfo.kronVec {n : Type u_1} (x y : n → ℂ) : n × n → ℂ

The product vector x ⊗ y on n × n.

Equations

• QuantumInfo.kronVec x y p = x p.1 * y p.2

theorem QuantumInfo.kronecker_vecMulVec_star {n : Type u_1} (x y : n → ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.vecMulVec x (star x)) (Matrix.vecMulVec y (star y)) = Matrix.vecMulVec (kronVec x y) (star (kronVec x y))

theorem QuantumInfo.star_kronVec_dotProduct {n : Type u_1} [Fintype n] (x y x' y' : n → ℂ) : star (kronVec x y) ⬝ᵥ kronVec x' y' = star x ⬝ᵥ x' * star y ⬝ᵥ y'

theorem QuantumInfo.vecMulVec_mulVec' {n : Type u_1} [Fintype n] {m : Type u_3} (u : m → ℂ) (v w : n → ℂ) : (Matrix.vecMulVec u v).mulVec w = (v ⬝ᵥ w) • u

theorem QuantumInfo.Channel.Broadcasts.kraus_mulVec_eq_smul_kronVec {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ψ : n → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) (h : Φ.Broadcasts (Matrix.vecMulVec ψ (star ψ))) (i : ι) : (Φ.kraus i).mulVec ψ = (star (kronVec ψ ψ) ⬝ᵥ (Φ.kraus i).mulVec ψ) • kronVec ψ ψ

A broadcast pure state is cloned: every Kraus operator sends ψ to a multiple of ψ ⊗ ψ (support confinement with the rank-one projector |ψ⟩⟨ψ|).

theorem QuantumInfo.Channel.star_dotProduct_eq_sum_kraus {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] (Φ : Channel n (n × n) ι) (φ ψ : n → ℂ) : star φ ⬝ᵥ ψ = ∑ i : ι, star ((Φ.kraus i).mulVec φ) ⬝ᵥ (Φ.kraus i).mulVec ψ

The trace-preservation identity read on two vectors: ⟨φ|ψ⟩ = ∑ᵢ ⟨Kᵢ φ|Kᵢ ψ⟩.

theorem QuantumInfo.norm_star_dotProduct_sq_le {m : Type u_3} [Fintype m] (x y : m → ℂ) : ‖star x ⬝ᵥ y‖ ^ 2 ≤ (star x ⬝ᵥ x).re * (star y ⬝ᵥ y).re

Cauchy–Schwarz for dotProduct: ‖⟨x|y⟩‖² ≤ ⟨x|x⟩ ⟨y|y⟩ (real parts).

theorem QuantumInfo.Channel.Broadcasts.star_dotProduct_eq_zero_or_norm_eq_one {n : Type u_1} {ι : Type u_2} [Fintype n] [DecidableEq n] [Fintype ι] {Φ : Channel n (n × n) ι} {ψ φ : n → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) (hφ : star φ ⬝ᵥ φ = 1) (h1 : Φ.Broadcasts (Matrix.vecMulVec ψ (star ψ))) (h2 : Φ.Broadcasts (Matrix.vecMulVec φ (star φ))) : star φ ⬝ᵥ ψ = 0 ∨ ‖star φ ⬝ᵥ ψ‖ = 1

★★ Two broadcast pure states are orthogonal or parallel. If one channel broadcasts both |ψ⟩⟨ψ| and |φ⟩⟨φ| (unit vectors), then ⟨φ|ψ⟩ = 0 or ‖⟨φ|ψ⟩‖ = 1: each Kraus operator clones both, and trace preservation gives ⟨φ|ψ⟩ = ⟨φ|ψ⟩² ∑ᵢ conj bᵢ aᵢ with |∑ᵢ conj bᵢ aᵢ| ≤ 1. This is the no-cloning theorem for channels, and the rank-one case of the hard half of BCFJS.

The support projector of a matrix

noncomputable def QuantumInfo.suppProj {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : Matrix n n ℂ

The orthogonal projector onto the range of A, as a matrix.

Equations

• QuantumInfo.suppProj A = Matrix.toEuclideanLin.symm ↑(Matrix.toEuclideanLin A).range.starProjection

theorem QuantumInfo.toEuclideanLin_suppProj {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : Matrix.toEuclideanLin (suppProj A) = ↑(Matrix.toEuclideanLin A).range.starProjection

theorem QuantumInfo.suppProj_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (x : n → ℂ) : (suppProj A).mulVec x = ((Matrix.toEuclideanLin A).range.starProjection (WithLp.toLp 2 x)).ofLp

theorem QuantumInfo.suppProj_mulVec_eq_self_iff {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (x : n → ℂ) : (suppProj A).mulVec x = x ↔ ∃ (y : n → ℂ), A.mulVec y = x

theorem QuantumInfo.suppProj_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : suppProj A * suppProj A = suppProj A

theorem QuantumInfo.suppProj_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : (suppProj A).IsHermitian

theorem QuantumInfo.suppProj_mul {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : suppProj A * A = A

theorem QuantumInfo.mul_suppProj_of_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) : A * suppProj A = A

Squared norms, and the top eigenvalue of a Hermitian matrix

def QuantumInfo.nsq {n : Type u_1} [Fintype n] (v : n → ℂ) : ℝ

‖v‖² as the real part of ⟨v|v⟩.

Equations

• QuantumInfo.nsq v = (star v ⬝ᵥ v).re

theorem QuantumInfo.nsq_eq_sum {n : Type u_1} [Fintype n] (v : n → ℂ) : nsq v = ∑ i : n, ‖v i‖ ^ 2

theorem QuantumInfo.nsq_nonneg {n : Type u_1} [Fintype n] (v : n → ℂ) : 0 ≤ nsq v

theorem QuantumInfo.nsq_eq_zero_iff {n : Type u_1} [Fintype n] (v : n → ℂ) : nsq v = 0 ↔ v = 0

theorem QuantumInfo.star_dotProduct_self_eq_nsq {n : Type u_1} [Fintype n] (v : n → ℂ) : star v ⬝ᵥ v = ↑(nsq v)

theorem QuantumInfo.nsq_mulVec {n : Type u_1} [Fintype n] {m : Type u_3} [Fintype m] (M : Matrix m n ℂ) (x : n → ℂ) : nsq (M.mulVec x) = (star x ⬝ᵥ (M.conjTranspose * M).mulVec x).re

theorem QuantumInfo.nsq_smul {n : Type u_1} [Fintype n] (c : ℂ) (v : n → ℂ) : nsq (c • v) = ‖c‖ ^ 2 * nsq v

theorem QuantumInfo.star_dotProduct_onbProj_mulVec {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (k : n) (z : n → ℂ) : star z ⬝ᵥ (onbProj b k).mulVec z = ↑(‖star (onbVec b k) ⬝ᵥ z‖ ^ 2)

⟨z| P_k |z⟩ = |⟨v_k|z⟩|² for the rank-one projector of a basis vector.

theorem QuantumInfo.IsHermitian.exists_top_eigenvalue {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {Q : Matrix n n ℂ} (hQ : Q.IsHermitian) : ∃ (μ : ℝ) (u : n → ℂ), star u ⬝ᵥ u = 1 ∧ Q.mulVec u = ↑μ • u ∧ ∀ (z : n → ℂ), (star z ⬝ᵥ Q.mulVec z).re ≤ μ * nsq z

The top eigenvalue of a Hermitian matrix bounds its Rayleigh quotient and is attained by a unit eigenvector: from Matrix.IsHermitian.eigenvectorBasis and completeness.

Projector inequalities

theorem QuantumInfo.posSemidef_of_isHermitian_of_re_nonneg {n : Type u_1} [Fintype n] {M : Matrix n n ℂ} (hM : M.IsHermitian) (h : ∀ (x : n → ℂ), 0 ≤ (star x ⬝ᵥ M.mulVec x).re) : M.PosSemidef

theorem QuantumInfo.nsq_mulVec_of_proj {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (x : n → ℂ) : nsq (P.mulVec x) = (star x ⬝ᵥ P.mulVec x).re

theorem QuantumInfo.one_sub_proj_isHermitian {n : Type u_1} [DecidableEq n] {P : Matrix n n ℂ} (hP : P.IsHermitian) : (1 - P).IsHermitian

theorem QuantumInfo.one_sub_proj_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP2 : P * P = P) : (1 - P) * (1 - P) = 1 - P

theorem QuantumInfo.nsq_one_sub_proj_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (x : n → ℂ) : nsq ((1 - P).mulVec x) = nsq x - nsq (P.mulVec x)

theorem QuantumInfo.nsq_proj_mulVec_le {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (x : n → ℂ) : nsq (P.mulVec x) ≤ nsq x

A projector is a contraction: ‖P x‖² ≤ ‖x‖².

theorem QuantumInfo.proj_mulVec_eq_self_of_nsq_eq {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (x : n → ℂ) (h : nsq (P.mulVec x) = nsq x) : P.mulVec x = x

Equality in the contraction forces P x = x.

The tensor bound Q ⊗ Q ≤ μ²

theorem QuantumInfo.re_star_dotProduct_kronecker_mulVec_le {n : Type u_1} [Fintype n] [DecidableEq n] {Q : Matrix n n ℂ} (hQ : Q.PosSemidef) {μ : ℝ} (hμ : 0 ≤ μ) (hbound : ∀ (z : n → ℂ), (star z ⬝ᵥ Q.mulVec z).re ≤ μ * nsq z) (x : n × n → ℂ) : (star x ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Q Q).mulVec x).re ≤ μ ^ 2 * nsq x

If ⟨z|Q|z⟩ ≤ μ ‖z‖² for a Hermitian Q ≥ 0 then ⟨x|Q ⊗ Q|x⟩ ≤ μ² ‖x‖²: the identity μ² − Q ⊗ Q = μ (μ − Q) ⊗ 1 + Q ⊗ (μ − Q) with both terms positive semidefinite.

BC3: broadcast states with disjoint supports have orthogonal supports

theorem QuantumInfo.Channel.sum_nsq_kraus_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) (x : n → ℂ) : ∑ i : ι, nsq ((Φ.kraus i).mulVec x) = nsq x

The squared norms of the Kraus images sum to the squared norm: ∑ᵢ ‖Kᵢ x‖² = ‖x‖².

theorem QuantumInfo.Channel.Broadcasts.mul_eq_zero_of_range_disjoint {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] {Φ : Channel n (n × n) ι} {A B : Matrix n n ℂ} (hA : A.PosSemidef) (hB : B.PosSemidef) (h1 : Φ.Broadcasts A) (h2 : Φ.Broadcasts B) (hdisj : ∀ (x : n → ℂ), (∃ (y : n → ℂ), A.mulVec y = x) → (∃ (z : n → ℂ), B.mulVec z = x) → x = 0) : B * A = 0

★★ BC3. Broadcast states with disjoint supports have orthogonal supports. If one channel broadcasts the positive semidefinite A and B and their ranges meet only in 0, then B A = 0. With P_A, P_B the support projectors and Q = P_A P_B P_A, the top eigenvalue μ of Q with unit eigenvector u ∈ range A and w = P_B u ∈ range B gives μ = ⟨w|u⟩ = ∑ᵢ ⟨Kᵢ w|Kᵢ u⟩; support confinement puts Kᵢ u in range A ⊗ range A and Kᵢ w in range B ⊗ range B, the tensor bound Q ⊗ Q ≤ μ² and Cauchy–Schwarz give μ ≤ μ √μ, so μ ∈ {0, 1}; μ = 1 would put u in both ranges, hence μ = 0, P_B P_A = 0 and B A = 0.

theorem Matrix.PosSemidef.mul_eq_zero_of_trace_mul_eq_zero {n : Type u_1} [Fintype n] [DecidableEq n] {X Y : Matrix n n ℂ} (hX : X.PosSemidef) (hY : Y.PosSemidef) (h : (X * Y).trace = 0) : X * Y = 0

Two positive semidefinite matrices with Tr (X Y) = 0 satisfy X Y = 0.

theorem QuantumInfo.Channel.one_sub_adjoint_kronecker_one_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) : (1 - Φ.adjoint (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1)).PosSemidef

The dual of P ⊗ 1 is contracted by 1 when P is a projector.

theorem QuantumInfo.Channel.one_sub_adjoint_one_kronecker_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) : (1 - Φ.adjoint (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P)).PosSemidef

theorem QuantumInfo.Channel.star_dotProduct_adjoint_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) (P : Matrix (n × n) (n × n) ℂ) (v : n → ℂ) : star v ⬝ᵥ (Φ.adjoint P).mulVec v = ∑ i : ι, star ((Φ.kraus i).mulVec v) ⬝ᵥ P.mulVec ((Φ.kraus i).mulVec v)

⟨v| Φ† P |v⟩ = ∑ᵢ ⟨Kᵢ v| P |Kᵢ v⟩.

theorem QuantumInfo.Channel.adjoint_kronecker_one_mulVec_eq_self {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) {v : n → ℂ} (hv : ∀ (i : ι), (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1).mulVec ((Φ.kraus i).mulVec v) = (Φ.kraus i).mulVec v) : (Φ.adjoint (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1)).mulVec v = v

The dual of P ⊗ 1 fixes every vector v all of whose Kraus images lie in range P ⊗ ℂⁿ.

theorem QuantumInfo.Channel.adjoint_one_kronecker_mulVec_eq_self {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] (Φ : Channel n (n × n) ι) {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) {v : n → ℂ} (hv : ∀ (i : ι), (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P).mulVec ((Φ.kraus i).mulVec v) = (Φ.kraus i).mulVec v) : (Φ.adjoint (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P)).mulVec v = v

theorem QuantumInfo.star_dotProduct_proj_mulVec_eq_nsq {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) (y : n → ℂ) : star y ⬝ᵥ P.mulVec y = ↑(nsq (P.mulVec y))

theorem QuantumInfo.kronecker_one_sub_left {n : Type u_1} [DecidableEq n] (P : Matrix n n ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (1 - P) 1 = 1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1

theorem QuantumInfo.kronecker_one_sub_right {n : Type u_1} [DecidableEq n] (P : Matrix n n ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (1 - P) = 1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P

theorem QuantumInfo.Channel.Broadcasts.kronecker_mulVec_kraus_mulVec_sub {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] {Φ : Channel n (n × n) ι} {τ : Matrix n n ℂ} (hτ : τ.PosSemidef) (h : Φ.Broadcasts τ) {PV : Matrix n n ℂ} (hPV : PV.IsHermitian) (hPV2 : PV * PV = PV) (hsub : suppProj τ * PV = PV) (hclone : ∀ (i : ι), Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) PV PV * (Φ.kraus i * PV) = Φ.kraus i * PV) (i : ι) (x : n → ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (suppProj τ - PV) (suppProj τ - PV)).mulVec ((Φ.kraus i).mulVec ((suppProj τ - PV).mulVec x)) = (Φ.kraus i).mulVec ((suppProj τ - PV).mulVec x)

BC4 (i): the complement of a cloned subspace inside the support is confined too. If Φ broadcasts the positive semidefinite τ, P_V is a projector onto a subspace V of the support of τ, and every Kraus operator maps V into V ⊗ V, then every Kraus operator maps W = supp τ ⊖ V into W ⊗ W. The dual Φ† (P_V ⊗ 1) fixes V, so its excess over P_V is positive semidefinite with zero trace against τ, hence kills the support; on W this says every Kᵢ w lies in V^⊥ ⊗ ℂⁿ, symmetrically in ℂⁿ ⊗ V^⊥, and support confinement finishes.

theorem QuantumInfo.traceRight_kronecker_mul_mul_kronecker {n : Type u_1} [Fintype n] [DecidableEq n] (A B C D : Matrix n n ℂ) (Y : Matrix (n × n) (n × n) ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B * Y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D).traceRight = A * (Y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (D * B)).traceRight * C

Tr_B ((A ⊗ B) Y (C ⊗ D)) = A · Tr_B (Y (1 ⊗ D B)) · C.

theorem QuantumInfo.traceLeft_kronecker_mul_mul_kronecker {n : Type u_1} [Fintype n] [DecidableEq n] (A B C D : Matrix n n ℂ) (Y : Matrix (n × n) (n × n) ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B * Y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D).traceLeft = B * (Y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (C * A) 1).traceLeft * D

Tr_A ((A ⊗ B) Y (C ⊗ D)) = B · Tr_A (Y (C A ⊗ 1)) · D.

theorem QuantumInfo.kraus_block_sandwich {n : Type u_1} [Fintype n] {K : Matrix (n × n) n ℂ} {P Q : Matrix n n ℂ} (hQ : Q.IsHermitian) {RP RQ : Matrix (n × n) (n × n) ℂ} (hRQ : RQ.IsHermitian) (hKP : RP * (K * P) = K * P) (hKQ : RQ * (K * Q) = K * Q) (τ : Matrix n n ℂ) : K * (P * τ * Q) * K.conjTranspose = RP * (K * (P * τ * Q) * K.conjTranspose) * RQ

One Kraus term of a cross block is sandwiched between the two block projectors.

theorem QuantumInfo.Channel.Broadcasts.block_split {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] {Φ : Channel n (n × n) ι} {τ : Matrix n n ℂ} (hτ : τ.PosSemidef) (h : Φ.Broadcasts τ) {PV : Matrix n n ℂ} (hPV : PV.IsHermitian) (hPV2 : PV * PV = PV) (hsub : suppProj τ * PV = PV) (hclone : ∀ (i : ι), Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) PV PV * (Φ.kraus i * PV) = Φ.kraus i * PV) : PV * τ * (suppProj τ - PV) = 0 ∧ Φ.Broadcasts (PV * τ * PV) ∧ Φ.Broadcasts ((suppProj τ - PV) * τ * (suppProj τ - PV))

★★ BC4: a cloned subspace splits a broadcast state into blocks, each broadcast. If Φ broadcasts the positive semidefinite τ, P_V is a projector onto a subspace V of the support S of τ, and every Kraus operator maps V into V ⊗ V, then with P_W = P_S − P_V: P_V τ P_W = 0 (so τ = P_V τ P_V + P_W τ P_W), and Φ broadcasts both blocks. The cross blocks Φ(P_V τ P_W) are sandwiched between P_V ⊗ P_V and P_W ⊗ P_W, whose partial traces vanish because P_W P_V = 0; the diagonal blocks are supported where they should be.

Eigen-expansions

theorem QuantumInfo.nsq_eq_sum_onb {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (z : n → ℂ) : nsq z = ∑ k : n, ‖star (onbVec b k) ⬝ᵥ z‖ ^ 2

Parseval: ‖z‖² = ∑ₖ |⟨b k|z⟩|².

theorem QuantumInfo.re_star_dotProduct_mulVec_eq_sum_onb {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) {Q : Matrix n n ℂ} {r : n → ℂ} (hdiag : ∀ (k : n), Q.mulVec (onbVec b k) = r k • onbVec b k) (z : n → ℂ) : (star z ⬝ᵥ Q.mulVec z).re = ∑ k : n, (r k * ↑(‖star (onbVec b k) ⬝ᵥ z‖ ^ 2)).re

The Rayleigh quotient of a matrix diagonal in b: ⟨z|Q|z⟩ = ∑ₖ rₖ |⟨b k|z⟩|².

theorem QuantumInfo.onbProj_mul_onbProj {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (j k : n) : onbProj b j * onbProj b k = if j = k then onbProj b k else 0

noncomputable def QuantumInfo.onbProjSet {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (K : Finset n) : Matrix n n ℂ

The projector onto the span of a subfamily of the basis.

Equations

• QuantumInfo.onbProjSet b K = ∑ k ∈ K, QuantumInfo.onbProj b k

theorem QuantumInfo.onbProjSet_isHermitian {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (K : Finset n) : (onbProjSet b K).IsHermitian

theorem QuantumInfo.onbProjSet_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (K : Finset n) : onbProjSet b K * onbProjSet b K = onbProjSet b K

theorem QuantumInfo.star_dotProduct_onbProjSet_mulVec {n : Type u_1} [Fintype n] (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (K : Finset n) (z : n → ℂ) : star z ⬝ᵥ (onbProjSet b K).mulVec z = ↑(∑ k ∈ K, ‖star (onbVec b k) ⬝ᵥ z‖ ^ 2)

BC5: the segment through two distinct states meets the boundary of the cone

theorem QuantumInfo.exists_re_star_dotProduct_neg_of_trace_eq_zero {n : Type u_1} [Fintype n] {d : Matrix n n ℂ} (hd : d.IsHermitian) (htr : d.trace = 0) (hne : d ≠ 0) : ∃ (v : n → ℂ), (star v ⬝ᵥ d.mulVec v).re < 0

A nonzero traceless Hermitian matrix has a direction of negative expectation.

theorem QuantumInfo.exists_boundary_point {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) (hρ1 : ρ.trace = 1) (hσ1 : σ.trace = 1) (hne : ρ ≠ σ) : ∃ (l : ℝ), 1 ≤ l ∧ (σ + ↑l • (ρ - σ)).PosSemidef ∧ ∃ (x : n → ℂ), (σ + ↑l • (ρ - σ)).mulVec x = 0 ∧ (ρ + σ).mulVec x ≠ 0

★★ BC5. The segment through two distinct states meets the boundary of the cone. For positive semidefinite ρ ≠ σ of trace one there is l ≥ 1 such that τ = σ + l (ρ − σ) = l ρ + (1 − l) σ is positive semidefinite and has a kernel vector outside the kernel of ρ + σ (so its support is strictly smaller). The set of such l is closed and bounded (the traceless ρ − σ has a negative direction), so its supremum l₁ belongs to it; if τ = f l₁ had no such kernel vector, f (l₁ + δ) would still be positive semidefinite for small δ (the eigenvectors of τ with eigenvalue 0 lie in ker (ρ + σ), hence in ker (ρ − σ), and on the rest the positive eigenvalues dominate), contradicting maximality.

Kernel facts

theorem QuantumInfo.suppProj_mulVec_eq_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (x : n → ℂ) : (suppProj A).mulVec x = 0 ↔ A.mulVec x = 0

The support projector of a Hermitian matrix vanishes exactly on its kernel.

theorem Matrix.PosSemidef.add_mulVec_eq_zero_iff {n : Type u_1} [Fintype n] {A B : Matrix n n ℂ} (hA : A.PosSemidef) (hB : B.PosSemidef) (x : n → ℂ) : (A + B).mulVec x = 0 ↔ A.mulVec x = 0 ∧ B.mulVec x = 0

A positive combination of positive semidefinite matrices vanishes on x iff both do.

theorem QuantumInfo.smul_mulVec_eq_zero_iff {n : Type u_1} [Fintype n] {A : Matrix n n ℂ} {c : ℂ} (hc : c ≠ 0) (x : n → ℂ) : (c • A).mulVec x = 0 ↔ A.mulVec x = 0

theorem QuantumInfo.rank_lt_rank_of_ker {n : Type u_1} [Fintype n] {A B : Matrix n n ℂ} (hAB : ∀ (x : n → ℂ), B.mulVec x = 0 → A.mulVec x = 0) {x : n → ℂ} (hx : A.mulVec x = 0) (hBx : B.mulVec x ≠ 0) : A.rank < B.rank

Strict rank comparison from a strict kernel inclusion.

The intersection projector, and intersections of tensor squares

theorem QuantumInfo.proj_posSemidef {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) : P.PosSemidef

theorem QuantumInfo.one_sub_proj_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : P.IsHermitian) (hP2 : P * P = P) : (1 - P).PosSemidef

noncomputable def QuantumInfo.interProj {n : Type u_1} [Fintype n] [DecidableEq n] (P₁ P₂ : Matrix n n ℂ) : Matrix n n ℂ

The projector onto the intersection of the ranges of two projectors: 1 − suppProj ((1 − P₁) + (1 − P₂)), since the kernel of the positive semidefinite sum is the intersection of the kernels.

Equations

• QuantumInfo.interProj P₁ P₂ = 1 - QuantumInfo.suppProj (1 - P₁ + (1 - P₂))

theorem QuantumInfo.interProj_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] (P₁ P₂ : Matrix n n ℂ) : (interProj P₁ P₂).IsHermitian

theorem QuantumInfo.interProj_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] (P₁ P₂ : Matrix n n ℂ) : interProj P₁ P₂ * interProj P₁ P₂ = interProj P₁ P₂

theorem QuantumInfo.interProj_mulVec_eq_self_iff {n : Type u_1} [Fintype n] [DecidableEq n] {P₁ P₂ : Matrix n n ℂ} (hP₁ : P₁.IsHermitian) (hP₁2 : P₁ * P₁ = P₁) (hP₂ : P₂.IsHermitian) (hP₂2 : P₂ * P₂ = P₂) (x : n → ℂ) : (interProj P₁ P₂).mulVec x = x ↔ P₁.mulVec x = x ∧ P₂.mulVec x = x

theorem QuantumInfo.mul_interProj {n : Type u_1} [Fintype n] [DecidableEq n] {P₁ P₂ : Matrix n n ℂ} (hP₁ : P₁.IsHermitian) (hP₁2 : P₁ * P₁ = P₁) (hP₂ : P₂.IsHermitian) (hP₂2 : P₂ * P₂ = P₂) : P₁ * interProj P₁ P₂ = interProj P₁ P₂ ∧ P₂ * interProj P₁ P₂ = interProj P₁ P₂

theorem QuantumInfo.kronecker_one_mulVec_apply {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (z : n × n → ℂ) (a c : n) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1).mulVec z (a, c) = A.mulVec (fun (a' : n) => z (a', c)) a

theorem QuantumInfo.one_kronecker_mulVec_apply {n : Type u_1} [Fintype n] [DecidableEq n] (B : Matrix n n ℂ) (z : n × n → ℂ) (a c : n) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B).mulVec z (a, c) = B.mulVec (fun (c' : n) => z (a, c')) c

theorem QuantumInfo.kronecker_one_mulVec_eq_self_of {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP2 : P * P = P) {z : n × n → ℂ} (h : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P P).mulVec z = z) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1).mulVec z = z ∧ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P).mulVec z = z

A vector fixed by P ⊗ P is fixed by P ⊗ 1 and by 1 ⊗ P.

theorem QuantumInfo.interProj_kronecker_mulVec_eq_self {n : Type u_1} [Fintype n] [DecidableEq n] {P₁ P₂ : Matrix n n ℂ} (hP₁ : P₁.IsHermitian) (hP₁2 : P₁ * P₁ = P₁) (hP₂ : P₂.IsHermitian) (hP₂2 : P₂ * P₂ = P₂) {z : n × n → ℂ} (h1 : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P₁ P₁).mulVec z = z) (h2 : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P₂ P₂).mulVec z = z) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (interProj P₁ P₂) (interProj P₁ P₂)).mulVec z = z

Intersections of tensor squares: a vector in S₁ ⊗ S₁ and in S₂ ⊗ S₂ lies in (S₁ ∩ S₂) ⊗ (S₁ ∩ S₂), column by column and row by row.

BC6: the rank induction, and the BCFJS theorem

theorem Matrix.PosSemidef.exists_smul_trace_one {n : Type u_1} [Fintype n] {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (h0 : ρ ≠ 0) : ∃ (t : ℝ), 0 < t ∧ (↑t⁻¹ • ρ).PosSemidef ∧ (↑t⁻¹ • ρ).trace = 1 ∧ ρ = ↑t • ↑t⁻¹ • ρ

Normalisation of a nonzero positive semidefinite matrix to trace one.

theorem QuantumInfo.Channel.Broadcasts.mul_comm_of_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_3} [Fintype ι] {Φ : Channel n (n × n) ι} {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) (h1 : Φ.Broadcasts ρ) (h2 : Φ.Broadcasts σ) : ρ * σ = σ * ρ

★★★ BCFJS, the hard half: broadcast states commute. If one channel broadcasts two positive semidefinite matrices, they commute. Strong induction on rank (ρ + σ): normalise to trace one, take the two boundary points τ₁, τ₂ of the segment (BC5; they are broadcast by linearity and [ρ, σ] is a positive multiple of [τ₁, τ₂]); with V the intersection of their supports (interProj), either V = 0 and BC3 gives τ₁ τ₂ = 0 = τ₂ τ₁, or V ≠ 0 is cloned by every Kraus operator (interProj_kronecker_mulVec_eq_self), BC4 splits each τᵢ into a V-block and a complementary block, both pairs of blocks are broadcast with strictly smaller rank of the sum (rank_lt_rank_of_ker, witnessed by the BC5 kernel vector and by a vector of V), so they commute by induction, and the cross products vanish.

theorem QuantumInfo.exists_channel_broadcasts_iff_commute {n : Type u} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : (∃ (κ : Type u) (x : Fintype κ) (Φ : Channel n (n × n) κ), Φ.Broadcasts ρ ∧ Φ.Broadcasts σ) ↔ ρ * σ = σ * ρ

★★★ BCFJS (Barnum–Caves–Fuchs–Jozsa–Schumacher 1996). Two positive semidefinite matrices can be broadcast by a single channel if and only if they commute.

theorem QuantumInfo.exists_orthonormalBasis_mulVec_eq_smul_of_pairwise_commute {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [Fintype κ] {ρ : κ → Matrix n n ℂ} (hρ : ∀ (k : κ), (ρ k).IsHermitian) (hc : ∀ (j k : κ), ρ j * ρ k = ρ k * ρ j) : ∃ (b : OrthonormalBasis n ℂ (EuclideanSpace ℂ n)) (r : κ → n → ℂ), ∀ (k : κ) (i : n), (ρ k).mulVec (onbVec b i) = r k i • onbVec b i

A pairwise-commuting family of Hermitian matrices has a joint orthonormal eigenbasis (Mathlib's LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, restricted to the finitely many joint eigenvalue functions and collected into a basis).

theorem QuantumInfo.exists_channel_broadcasts_of_pairwise_commute {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [Fintype κ] {ρ : κ → Matrix n n ℂ} (hρ : ∀ (k : κ), (ρ k).IsHermitian) (hc : ∀ (j k : κ), ρ j * ρ k = ρ k * ρ j) : ∃ (Φ : Channel n (n × n) n), ∀ (k : κ), Φ.Broadcasts (ρ k)

★★ A pairwise-commuting family of Hermitian matrices can be broadcast by one channel: the copier in a joint eigenbasis.

theorem QuantumInfo.exists_channel_broadcasts_family_iff_pairwise_commute {n : Type u} [Fintype n] [DecidableEq n] {κ : Type u_3} [Fintype κ] {ρ : κ → Matrix n n ℂ} (hρ : ∀ (k : κ), (ρ k).PosSemidef) : (∃ (ι : Type u) (x : Fintype ι) (Φ : Channel n (n × n) ι), ∀ (k : κ), Φ.Broadcasts (ρ k)) ↔ ∀ (j k : κ), ρ j * ρ k = ρ k * ρ j

★★★ BCFJS for families. A finite family of positive semidefinite matrices can be broadcast by a single channel iff its members pairwise commute.