Partial trace

DefinitionPartial trace over the first factor#✓fully proved

The partial trace over the first factor: ∑ i, A (i, j) (i, j').

def partialTraceLeft [Fintype m] [Fintype n]
    (A : Matrix (m × n) (m × n) 𝕜) : Matrix n n 𝕜 :=
  Matrix.of fun j j' => ∑ i, A (i, j) (i, j')

Used by 4

Used byLeft partial trace of a rank-one matrix · Left partial trace preserves positive semidefiniteness · Left partial trace is adjoint to identity amplification · Left partial trace of a density matrix has trace one

DefinitionPartial trace over the second factor#✓fully proved

The partial trace over the second factor: ∑ j, A (i, j) (i', j).

def partialTraceRight [Fintype m] [Fintype n]
    (A : Matrix (m × n) (m × n) 𝕜) : Matrix m m 𝕜 :=
  Matrix.of fun i i' => ∑ j, A (i, j) (i', j)

Used by 4

Used byRight partial trace of a rank-one matrix · Right partial trace preserves positive semidefiniteness · Right partial trace is adjoint to identity amplification · Right partial trace of a density matrix has trace one

TheoremLeft partial trace of a density matrix has trace one#✓fully proved

The partial trace of a density matrix has trace 1.

theorem trace_partialTraceLeft_of_trace_eq_one [Fintype m] [Fintype n]
    {A : Matrix (m × n) (m × n) 𝕜}
    (hA : Matrix.trace A = 1) : Matrix.trace (partialTraceLeft A) = 1

Uses 1

Statement usesPartial trace over the first factor

TheoremRight partial trace of a density matrix has trace one#✓fully proved

The partial trace of a density matrix has trace 1.

theorem trace_partialTraceRight_of_trace_eq_one [Fintype m] [Fintype n]
    {A : Matrix (m × n) (m × n) 𝕜}
    (hA : Matrix.trace A = 1) : Matrix.trace (partialTraceRight A) = 1

Uses 1

Statement usesPartial trace over the second factor

TheoremLeft partial trace of a rank-one matrix#✓fully proved

The partial trace of a rank-one positive semidefinite matrix is the sum of the rank-one positive semidefinite matrices of its slices.

theorem partialTraceLeft_vecMulVec_star [Fintype m] [Fintype n] (u : m × n → 𝕜) :
    partialTraceLeft (Matrix.vecMulVec u (star u)) =
      ∑ i, Matrix.vecMulVec (fun j => u (i, j)) (star fun j => u (i, j))

Uses 1 · Used by 1

Statement usesPartial trace over the first factor

Used byLeft partial trace preserves positive semidefiniteness

TheoremRight partial trace of a rank-one matrix#✓fully proved

The partial trace of a rank-one positive semidefinite matrix is the sum of the rank-one positive semidefinite matrices of its slices.

theorem partialTraceRight_vecMulVec_star [Fintype m] [Fintype n] (u : m × n → 𝕜) :
    partialTraceRight (Matrix.vecMulVec u (star u)) =
      ∑ j, Matrix.vecMulVec (fun i => u (i, j)) (star fun i => u (i, j))

Uses 1 · Used by 1

Statement usesPartial trace over the second factor

Used byRight partial trace preserves positive semidefiniteness

TheoremLeft partial trace preserves positive semidefiniteness#✓fully proved

The partial trace over the first factor preserves positive semidefiniteness.

theorem posSemidef_partialTraceLeft [Fintype m] [Fintype n]
    {A : Matrix (m × n) (m × n) 𝕜}
    (hA : A.PosSemidef) : (partialTraceLeft A).PosSemidef

Uses 2

Statement usesPartial trace over the first factor

Proof usesLeft partial trace of a rank-one matrix

TheoremRight partial trace preserves positive semidefiniteness#✓fully proved

The partial trace over the second factor preserves positive semidefiniteness.

theorem posSemidef_partialTraceRight [Fintype m] [Fintype n]
    {A : Matrix (m × n) (m × n) 𝕜}
    (hA : A.PosSemidef) : (partialTraceRight A).PosSemidef

Uses 2

Statement usesPartial trace over the second factor

Proof usesRight partial trace of a rank-one matrix

TheoremLeft partial trace is adjoint to identity amplification#✓fully proved

The partial trace over the first factor is adjoint to amplification by the identity, in the trace pairing.

theorem trace_partialTraceLeft_mul [Fintype m] [Fintype n] [DecidableEq m]
    (A : Matrix (m × n) (m × n) 𝕜) (B : Matrix n n 𝕜) :
    Matrix.trace (partialTraceLeft A * B)
      = Matrix.trace (A * ((1 : Matrix m m 𝕜) ⊗ₖ B))

Uses 1

Statement usesPartial trace over the first factor

TheoremRight partial trace is adjoint to identity amplification#✓fully proved

The partial trace over the second factor is adjoint to amplification by the identity, in the trace pairing.

theorem trace_partialTraceRight_mul [Fintype m] [Fintype n] [DecidableEq n]
    (A : Matrix (m × n) (m × n) 𝕜) (C : Matrix m m 𝕜) :
    Matrix.trace (partialTraceRight A * C)
      = Matrix.trace (A * (C ⊗ₖ (1 : Matrix n n 𝕜)))

Uses 1

Statement usesPartial trace over the second factor

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.