Documentation

Oseledets.OperatorEntropy.PartialTrace

Partial traces on raw matrices #

This module defines the partial trace of an operator on a bipartite system nA ⊗ nB, working directly with raw Matrix (nA × nB) (nA × nB) ℂ (no density-matrix wrapper). We record that the partial trace preserves the total trace, is Hermitian on Hermitian inputs, and — the operative fact for quantum information — sends positive semidefinite operators to positive semidefinite operators.

The positivity is proved through an explicit completely positive decomposition: Tr_B M is the sum over j of the compressions of M to the j-th block, i.e. the conjugations of M by the block-inclusion isometries Eⱼᴴ : i ↦ (i, j). Each compression is positive semidefinite (Matrix.PosSemidef.submatrix), and a finite sum of positive semidefinite matrices is positive semidefinite. This is the Kraus / Stinespring picture of the partial trace as a CP map.

source
noncomputable def Oseledets.OperatorEntropy.partialTraceRight {nA : Type u_1} {nB : Type u_2} [Fintype nB] (M : Matrix (nA × nB) (nA × nB) ℂ) :
Matrix nA nA ℂ

Partial trace over the right (B) factor: (Tr_B M) i i' = ∑ⱼ M (i,j) (i',j).

Equations
Instances For
    source
    noncomputable def Oseledets.OperatorEntropy.partialTraceLeft {nA : Type u_1} {nB : Type u_2} [Fintype nA] (M : Matrix (nA × nB) (nA × nB) ℂ) :
    Matrix nB nB ℂ

    Partial trace over the left (A) factor: (Tr_A M) j j' = ∑ᵢ M (i,j) (i,j').

    Equations
    Instances For
      source
      theorem Oseledets.OperatorEntropy.partialTraceRight_apply {nA : Type u_1} {nB : Type u_2} [Fintype nB] (M : Matrix (nA × nB) (nA × nB) ℂ) (i i' : nA) :
      partialTraceRight M i i' = ∑ j : nB, M (i, j) (i', j)

      Entrywise formula for the right partial trace.

      source
      theorem Oseledets.OperatorEntropy.partialTraceLeft_apply {nA : Type u_1} {nB : Type u_2} [Fintype nA] (M : Matrix (nA × nB) (nA × nB) ℂ) (j j' : nB) :
      partialTraceLeft M j j' = ∑ i : nA, M (i, j) (i, j')

      Entrywise formula for the left partial trace.

      source
      theorem Oseledets.OperatorEntropy.trace_partialTraceRight {nA : Type u_1} {nB : Type u_2} [Fintype nA] [Fintype nB] (M : Matrix (nA × nB) (nA × nB) ℂ) :
      (partialTraceRight M).trace = M.trace

      The partial trace over B preserves the total trace: Tr (Tr_B M) = Tr M.

      source
      theorem Oseledets.OperatorEntropy.trace_partialTraceLeft {nA : Type u_1} {nB : Type u_2} [Fintype nA] [Fintype nB] (M : Matrix (nA × nB) (nA × nB) ℂ) :
      (partialTraceLeft M).trace = M.trace

      The partial trace over A preserves the total trace: Tr (Tr_A M) = Tr M.

      source
      theorem Oseledets.OperatorEntropy.IsHermitian.partialTraceRight {nA : Type u_1} {nB : Type u_2} [Fintype nB] {M : Matrix (nA × nB) (nA × nB) ℂ} (hM : M.IsHermitian) :
      (OperatorEntropy.partialTraceRight M).IsHermitian

      The partial trace over B of a Hermitian operator is Hermitian.

      source
      theorem Oseledets.OperatorEntropy.IsHermitian.partialTraceLeft {nA : Type u_1} {nB : Type u_2} [Fintype nA] {M : Matrix (nA × nB) (nA × nB) ℂ} (hM : M.IsHermitian) :
      (OperatorEntropy.partialTraceLeft M).IsHermitian

      The partial trace over A of a Hermitian operator is Hermitian.

      Completely positive (compression) decomposition #

      Tr_B M = ∑ⱼ M.submatrix (· ↦ (·, j)) (· ↦ (·, j)): the partial trace is the sum of the compressions of M to the diagonal j-th blocks. The reindexing map a ↦ (a, j) is the block-inclusion isometry, and M.submatrix e e is the conjugation Eᴴ M E; this is exactly the Kraus form of the partial trace, written without matrix multiplication.

      source
      theorem Oseledets.OperatorEntropy.partialTraceRight_eq_sum_submatrix {nA : Type u_1} {nB : Type u_2} [Fintype nB] (M : Matrix (nA × nB) (nA × nB) ℂ) :
      partialTraceRight M = ∑ j : nB, M.submatrix (fun (a : nA) => (a, j)) fun (a : nA) => (a, j)

      Compression / Kraus decomposition of the right partial trace.

      source
      theorem Oseledets.OperatorEntropy.partialTraceLeft_eq_sum_submatrix {nA : Type u_1} {nB : Type u_2} [Fintype nA] (M : Matrix (nA × nB) (nA × nB) ℂ) :
      partialTraceLeft M = ∑ i : nA, M.submatrix (fun (b : nB) => (i, b)) fun (b : nB) => (i, b)

      Compression / Kraus decomposition of the left partial trace.

      source
      theorem Oseledets.OperatorEntropy.PosSemidef.partialTraceRight {nA : Type u_1} {nB : Type u_2} [Fintype nB] {M : Matrix (nA × nB) (nA × nB) ℂ} (hM : M.PosSemidef) :
      (OperatorEntropy.partialTraceRight M).PosSemidef

      The partial trace over B of a positive semidefinite operator is positive semidefinite.

      source
      theorem Oseledets.OperatorEntropy.PosSemidef.partialTraceLeft {nA : Type u_1} {nB : Type u_2} [Fintype nA] {M : Matrix (nA × nB) (nA × nB) ℂ} (hM : M.PosSemidef) :
      (OperatorEntropy.partialTraceLeft M).PosSemidef

      The partial trace over A of a positive semidefinite operator is positive semidefinite.