Quantities of quantum relative entropy, namely the (standard) quantum relative entropy, and generalizations such as sandwiched Rényi relative entropy.

noncomputable def Matrix.opNorm {m : Type u_5} {n : Type u_6} [Fintype m] [Fintype n] [DecidableEq n] {𝕜 : Type u_12} [RCLike 𝕜] (A : Matrix m n 𝕜) : ℝ

The operator norm of a matrix, with respect to the Euclidean norm (l2 norm) on the domain and codomain.

Equations

• A.opNorm = ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)‖

theorem Matrix.isometry_preserves_norm {m : Type u_5} {n : Type u_6} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {𝕜 : Type u_12} [RCLike 𝕜] (A : Matrix n m 𝕜) (hA : A.Isometry) (x : EuclideanSpace 𝕜 m) : ‖(toEuclideanLin A) x‖ = ‖x‖

theorem Matrix.opNorm_isometry {m : Type u_5} {n : Type u_6} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {𝕜 : Type u_12} [RCLike 𝕜] [Nonempty m] (A : Matrix n m 𝕜) (hA : A.Isometry) : A.opNorm = 1

def map_to_tensor_MES (d₁ : Type u_2) (d₂ : Type u_3) [DecidableEq d₁] [DecidableEq d₂] : Matrix ((d₁ × d₂) × d₂) d₁ ℂ

The matrix representation of the map $v \mapsto v \otimes \sum_k |k\rangle|k\rangle$. The output index is (d1 \times d2) \times d2.

Equations

• map_to_tensor_MES d₁ d₂ = Matrix.of fun (x : (d₁ × d₂) × d₂) (l : d₁) => match x with | ((i, j), k) => if i = l ∧ j = k then 1 else 0

theorem map_to_tensor_MES_prop {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (A : Matrix (d₁ × d₂) (d₁ × d₂) ℂ) : (map_to_tensor_MES d₁ d₂).conjTranspose * A.kronecker 1 * map_to_tensor_MES d₁ d₂ = A.traceRight

noncomputable def V_rho {dA : Type u_7} {dB : Type u_8} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρAB : HermitianMat (dA × dB) ℂ) : Matrix ((dA × dB) × dB) dA ℂ

The isometry V_rho from the paper.

Equations

• V_rho ρAB = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑ρAB.sqrt) 1 * map_to_tensor_MES dA dB * ↑ρAB.traceRight⁻¹.sqrt

noncomputable def V_sigma {dB : Type u_8} {dC : Type u_9} [Fintype dB] [Fintype dC] [DecidableEq dB] [DecidableEq dC] (σBC : HermitianMat (dB × dC) ℂ) : Matrix (dB × dB × dC) dC ℂ

The isometry V_sigma from the paper.

Equations

• V_sigma σBC = (Matrix.reindex ((Equiv.prodComm (dC × dB) dB).trans ((Equiv.refl dB).prodCongr (Equiv.prodComm dC dB))) (Equiv.refl dC)) (V_rho (σBC.reindex (Equiv.prodComm dB dC)))

theorem V_rho_conj_mul_self_eq {dA : Type u_7} {dB : Type u_8} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρAB : HermitianMat (dA × dB) ℂ) (hρ : (↑ρAB).PosDef) : have ρA := ρAB.traceRight; have ρA_inv_sqrt := ↑ρA⁻¹.sqrt; (V_rho ρAB).conjTranspose * V_rho ρAB = ρA_inv_sqrt * ↑ρAB.traceRight * ρA_inv_sqrt

V_rho^H * V_rho simplifies to sandwiching the traceRight by the inverse square root.

theorem PosDef_traceRight {dA : Type u_7} {dB : Type u_8} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [Nonempty dB] (A : HermitianMat (dA × dB) ℂ) (hA : (↑A).PosDef) : (↑A.traceRight).PosDef

The partial trace (left) of a positive definite matrix is positive definite.

theorem PosDef_traceLeft {dA : Type u_7} {dB : Type u_8} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [Nonempty dA] (A : HermitianMat (dA × dB) ℂ) (hA : (↑A).PosDef) : (↑A.traceLeft).PosDef

theorem V_rho_isometry {dA : Type u_7} {dB : Type u_8} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [Nonempty dB] (ρAB : HermitianMat (dA × dB) ℂ) (hρ : (↑ρAB).PosDef) : (V_rho ρAB).conjTranspose * V_rho ρAB = 1

V_rho is an isometry.

theorem V_sigma_isometry {dB : Type u_8} {dC : Type u_9} [Fintype dB] [Fintype dC] [DecidableEq dB] [DecidableEq dC] [Nonempty dB] (σBC : HermitianMat (dB × dC) ℂ) (hσ : (↑σBC).PosDef) : (V_sigma σBC).conjTranspose * V_sigma σBC = 1

V_sigma is an isometry.

noncomputable def W_mat {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ) : Matrix ((dA × dB) × dC) ((dA × dB) × dC) ℂ

The operator W from the paper, defined as a matrix product.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.opNorm_mul_le {l : Type u_16} {m : Type u_17} {n : Type u_18} {𝕜 : Type u_19} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [RCLike 𝕜] (A : Matrix l m 𝕜) (B : Matrix m n 𝕜) : (A * B).opNorm ≤ A.opNorm * B.opNorm

The operator norm of a matrix product is at most the product of the operator norms.

theorem Matrix.opNorm_reindex_proven {𝕜 : Type u_12} [RCLike 𝕜] {l : Type u_16} {m : Type u_17} {n : Type u_18} {p : Type u_19} [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (e : m ≃ l) (f : n ≃ p) (A : Matrix m n 𝕜) : ((reindex e f) A).opNorm = A.opNorm

noncomputable def U_rho {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρAB : HermitianMat (dA × dB) ℂ) : Matrix (((dA × dB) × dB) × dC) (dA × dC) ℂ

Define U_rho as the Kronecker product of V_rho and the identity.

Equations

• U_rho ρAB = (V_rho ρAB).kronecker 1

noncomputable def U_sigma {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (σBC : HermitianMat (dB × dC) ℂ) : Matrix (dA × dB × dB × dC) (dA × dC) ℂ

Define U_sigma as the Kronecker product of the identity and V_sigma.

Equations

• U_sigma σBC = Matrix.kronecker 1 (V_sigma σBC)

theorem Matrix.opNorm_conjTranspose_eq_opNorm {𝕜 : Type u_12} [RCLike 𝕜] {m : Type u_16} {n : Type u_17} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n 𝕜) : A.conjTranspose.opNorm = A.opNorm

The operator norm of the conjugate transpose is equal to the operator norm.

theorem isometry_mul_conjTranspose_le_one {m : Type u_16} {n : Type u_17} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (V : Matrix m n ℂ) (hV : V.conjTranspose * V = 1) : V * V.conjTranspose ≤ 1

theorem conjTranspose_isometry_mul_isometry_le_one {m : Type u_16} {n : Type u_17} {k : Type u_18} [Fintype m] [Fintype n] [Fintype k] [DecidableEq m] [DecidableEq n] [DecidableEq k] (A : Matrix k m ℂ) (B : Matrix k n ℂ) (hA : A.conjTranspose * A = 1) (hB : B.conjTranspose * B = 1) : (A.conjTranspose * B).conjTranspose * (A.conjTranspose * B) ≤ 1

Helper lemmas for operator_ineq_SSA

theorem HermitianMat.reindex_le_reindex_iff {d : Type u_16} {d₂ : Type u_17} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d ≃ d₂) (A B : HermitianMat d ℂ) : A.reindex e ≤ B.reindex e ↔ A ≤ B

theorem HermitianMat.inv_kronecker {m : Type u_16} {n : Type u_17} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [Nonempty m] [Nonempty n] (A : HermitianMat m ℂ) (B : HermitianMat n ℂ) [A.NonSingular] [B.NonSingular] : (A.kronecker B)⁻¹ = A⁻¹.kronecker B⁻¹

theorem HermitianMat.inv_reindex {d : Type u_16} {d₂ : Type u_17} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (A : HermitianMat d ℂ) (e : d ≃ d₂) : (A.reindex e)⁻¹ = A⁻¹.reindex e

theorem HermitianMat.PosDef_kronecker {m : Type u_16} {n : Type u_17} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : HermitianMat m ℂ) (B : HermitianMat n ℂ) (hA : (↑A).PosDef) (hB : (↑B).PosDef) : (↑(A.kronecker B)).PosDef

theorem HermitianMat.PosDef_reindex {d : Type u_16} {d₂ : Type u_17} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (A : HermitianMat d ℂ) (e : d ≃ d₂) (hA : (↑A).PosDef) : (↑(A.reindex e)).PosDef

@[reducible, inline]

abbrev BigIdx (dA : Type u_19) (dB : Type u_20) (dC : Type u_21) : Type (max (max u_20 u_19) u_21 u_20)

Equations

• BigIdx dA dB dC = (((dA × dB) × dB) × dB × dC)

@[reducible, inline]

abbrev SmallIdx (dA : Type u_19) (dB : Type u_20) (dC : Type u_21) : Type (max (max u_20 u_19) u_21)

Equations

• SmallIdx dA dB dC = ((dA × dB) × dC)

@[reducible, inline]

abbrev MidIdx (dA : Type u_19) (dB : Type u_20) (dC : Type u_21) : Type (max (max u_20 u_19) u_21 u_20)

Equations

• MidIdx dA dB dC = ((dA × dB) × dB × dB × dC)

theorem W_mat_sq_le_one {dA : Type u_16} {dB : Type u_17} {dC : Type u_18} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] [Nonempty dA] [Nonempty dB] [Nonempty dC] (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ) (hρ : (↑ρAB).PosDef) (hσ : (↑σBC).PosDef) : (W_mat ρAB σBC).conjTranspose * W_mat ρAB σBC ≤ 1

Core inequality: W†W ≤ I. This is the key step, following from the isometry argument: V_rho ⊗ I_C and I_A ⊗ V_sigma are isometries, their cross product has norm ≤ 1, and the result can be related to W_mat through the MES computation (Eq. 6 in Lin-Kim-Hsieh).

theorem intermediate_ineq {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] [Nonempty dA] [Nonempty dB] [Nonempty dC] (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ) (hρ : (↑ρAB).PosDef) (hσ : (↑σBC).PosDef) : ρAB.kronecker σBC.traceLeft⁻¹ ≤ (ρAB.traceRight.kronecker σBC⁻¹).reindex (Equiv.prodAssoc dA dB dC).symm

The intermediate operator inequality: ρ_AB ⊗ σ_C⁻¹ ≤ (ρ_A ⊗ σ_BC⁻¹).reindex(assoc⁻¹). This is derived from W_mat_sq_le_one by algebraic manipulation (conjugation and simplification).

theorem operator_ineq_SSA {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] [Nonempty dA] [Nonempty dB] [Nonempty dC] (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ) (hρ : (↑ρAB).PosDef) (hσ : (↑σBC).PosDef) : ρAB.traceRight⁻¹.kronecker σBC ≤ (ρAB⁻¹.kronecker σBC.traceLeft).reindex (Equiv.prodAssoc dA dB dC)

Operator extension of SSA (Main result of Lin-Kim-Hsieh). For positive definite ρ_AB and σ_BC: ρ_A⁻¹ ⊗ σ_BC ≤ ρ_AB⁻¹ ⊗ σ_C where ρ_A = Tr_B(ρ_AB) and σ_C = Tr_B(σ_BC), and the RHS is reindexed via the associator (dA × dB) × dC ≃ dA × (dB × dC).

Weak monotonicity and SSA proof infrastructure

theorem Sᵥₙ_wm {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft.traceLeft ≤ Sᵥₙ ρ.assoc'.traceRight + Sᵥₙ ρ.traceLeft

Weak monotonicity, version with partial traces.

theorem Sᵥₙ_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : have ρ₁₂ := ρ₁₂₃.assoc'.traceRight; have ρ₂₃ := ρ₁₂₃.traceLeft; have ρ₂ := ρ₁₂₃.traceLeft.traceRight; Sᵥₙ ρ₁₂₃ + Sᵥₙ ρ₂ ≤ Sᵥₙ ρ₁₂ + Sᵥₙ ρ₂₃

Strong subadditivity on a tripartite system

theorem Sᵥₙ_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : Sᵥₙ ρ ≤ Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft

"Ordinary" subadditivity of von Neumann entropy

theorem Sᵥₙ_pure_tripartite_triangle {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ψ : Ket ((d₁ × d₂) × d₃)) : Sᵥₙ (MState.pure ψ).traceRight.traceRight ≤ Sᵥₙ (MState.pure ψ).traceRight.traceLeft + Sᵥₙ (MState.pure ψ).traceLeft

Triangle inequality for pure tripartite states: S(A) ≤ S(B) + S(C).

theorem Sᵥₙ_triangle_ineq_one_way {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : Sᵥₙ ρ.traceRight ≤ Sᵥₙ ρ.traceLeft + Sᵥₙ ρ

One direction of the Araki-Lieb triangle inequality: S(A) ≤ S(B) + S(AB).

theorem Sᵥₙ_triangle_subaddivity {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : |Sᵥₙ ρ.traceRight - Sᵥₙ ρ.traceLeft| ≤ Sᵥₙ ρ

Araki-Lieb triangle inequality on von Neumann entropy

theorem Sᵥₙ_weak_monotonicity {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : have ρAB := ρ.assoc'.traceRight; have ρAC := ρ.SWAP.assoc.traceLeft.SWAP; 0 ≤ qConditionalEnt ρAB + qConditionalEnt ρAC

Weak monotonicity of quantum conditional entropy: S(A|B) + S(A|C) ≥ 0.

theorem qConditionalEnt_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : qConditionalEnt ρ₁₂₃ ≤ qConditionalEnt ρ₁₂₃.assoc'.traceRight

Strong subadditivity, stated in terms of conditional entropies. Also called the data processing inequality. H(A|BC) ≤ H(A|B).

theorem qMutualInfo_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : qMutualInfo ρ₁₂₃ ≥ qMutualInfo ρ₁₂₃.assoc'.traceRight

Strong subadditivity, stated in terms of quantum mutual information. I(A;BC) ≥ I(A;B).

theorem qcmi_nonneg {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : 0 ≤ qcmi ρ

The quantum conditional mutual information QCMI is nonnegative.

theorem qcmi_le_2_log_dim {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : qcmi ρ ≤ 2 * Real.log ↑(Fintype.card dA)

The quantum conditional mutual information QCMI ρABC is at most 2 log dA.

theorem qcmi_le_2_log_dim' {dA : Type u_13} {dB : Type u_14} {dC : Type u_15} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : qcmi ρ ≤ 2 * Real.log ↑(Fintype.card dC)

The quantum conditional mutual information QCMI ρABC is at most 2 log dC.