Manuscript En03-A@1 · En03-A.tex · lemma · 5398614e

Lemma: Channels commute with spectator restriction

Spectator-extension invariance › Arbitrary extensions · lines 940–956 · proof included or linked

En03-A@1#lem:trace, En03-A@1#eq:trace-channel

For $Ψ : L (H_{Γ}) \to L (H_{Γ^{'}})$ ,

Tr_{N} [(Ψ \otimes id_{N}) (ρ)] = Ψ (Tr_{N} ρ) .

Proof. For every output observable $A$ , both sides have expectation

Tr ((Ψ^{*} (A) \otimes I_{N}) ρ) = Tr (Ψ^{*} (A) Tr_{N} ρ) .

Displayed formulas in this passage

En03-A@1#eq:trace-channel · line 943
$Tr_{N} [(Ψ \otimes id_{N}) (ρ)] = Ψ (Tr_{N} ρ) .$
unlabeled · line 952
$Tr ((Ψ^{*} (A) \otimes I_{N}) ρ) = Tr (Ψ^{*} (A) Tr_{N} ρ) .$