Finite pairs are closed under ancilla extensions and under the exchange of the players

The Pauli basis analysis applies the low-individual-degree hypothesis in the ancilla extensions M.expand e of the model it works in (QLD.soundIn_of_lidt), and the answer-reduction and Pauli basis analyses are stated for both orders of the players. So the class of finite pairs (MIPRE/Foundations/FinitePair.lean) has to be closed under both, which this file shows (lem:finite-pair-expand).

• Extensions. The players' operators of M.expand e are X ⊗ 1_β and 1_α ⊗ Y for matrices X over 𝒜 and Y over ℬ. An operator commuting with every 1_α ⊗ Y commutes with the register's matrix units and with f ⊗ 1 for every operator f of the second player, so it is X ⊗ 1_β with entries in the commutant of the second player's operators (OperatorMatrix.exists_eq_toCLM_liftLeft), which are the first player's; and symmetrically. The trace of the first player's algebra is the normalized trace of the matrices, τ'(X ⊗ 1) = |α × β|⁻¹ ∑ₚ τ((X ⊗ 1)ₚₚ) = |α|⁻¹ ∑ᵢ τ(Xᵢᵢ), given by the vectors |α × β|^{-1/2} gₖ ⊗ eₚ (VecTrace.ampl); it is tracial because τ is, and faithful because the vectors of τ separate the entries.
• The exchange of the players swaps the two conditions.

Faithful tracial states on matrices of operators

noncomputable def MIPRE.VecTrace.ofFintype {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} {κ : Type u_2} [Fintype κ] (g : κ → H) (norm_sq_sum : ∑ k : κ, ‖g k‖ ^ 2 = 1) (trace_mul_comm : ∀ x ∈ s, ∀ y ∈ s, ∑ k : κ, inner ℂ (g k) ((x * y) (g k)) = ∑ k : κ, inner ℂ (g k) ((y * x) (g k))) (separating : ∀ x ∈ s, (∀ (k : κ), x (g k) = 0) → x = 0) : VecTrace s

A faithful tracial state given by vectors indexed by any finite type, numbered.

Equations

• MIPRE.VecTrace.ofFintype g norm_sq_sum trace_mul_comm separating = { n := Fintype.card κ, g := g ∘ ⇑(Fintype.equivFin κ).symm, norm_sq_sum := ⋯, trace_mul_comm := ⋯, separating := ⋯ }

def MIPRE.VecTrace.mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s t : Set (H →L[ℂ] H)} (τ : VecTrace t) (h : s ⊆ t) : VecTrace s

A faithful tracial state on a set is one on each of its subsets.

Equations

• τ.mono h = { n := τ.n, g := τ.g, norm_sq_sum := ⋯, trace_mul_comm := ⋯, separating := ⋯ }

noncomputable def MIPRE.VecTrace.amplVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) (m : Fin τ.n × ι) : OperatorMatrix.Ampl ι H

The vectors of the amplified state: |ι|^{-1/2} gₖ ⊗ eₚ.

Equations

• τ.amplVec m = ↑√(↑(Fintype.card ι))⁻¹ • (MIPRE.OperatorMatrix.emb m.2) (τ.g m.1)

theorem MIPRE.VecTrace.sum_inner_amplVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) (Z : Matrix ι ι (H →L[ℂ] H)) : ∑ m : Fin τ.n × ι, inner ℂ (τ.amplVec m) ((OperatorMatrix.toCLM Z) (τ.amplVec m)) = (↑(Fintype.card ι))⁻¹ * ∑ p : ι, ∑ k : Fin τ.n, inner ℂ (τ.g k) ((Z p p) (τ.g k))

The amplified state of the operator of a matrix is the normalized trace of the matrix, |ι|⁻¹ ∑ₚ τ(Zₚₚ).

theorem MIPRE.VecTrace.sum_trace_mul_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) {Z W : Matrix ι ι (H →L[ℂ] H)} (hZ : Z ∈ s.matrix) (hW : W ∈ s.matrix) : ∑ p : ι, ∑ k : Fin τ.n, inner ℂ (τ.g k) (((Z * W) p p) (τ.g k)) = ∑ p : ι, ∑ k : Fin τ.n, inner ℂ (τ.g k) (((W * Z) p p) (τ.g k))

The normalized trace of a product of matrices over s is tracial when τ is.

noncomputable def MIPRE.VecTrace.ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Nonempty ι] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) : VecTrace (OperatorMatrix.toCLM '' s.matrix)

The normalized trace of matrices over a set carrying a faithful tracial state: the operators of the ι × ι matrices with entries in s carry the faithful tracial state τ'(Z) = |ι|⁻¹ ∑ₚ τ(Zₚₚ), given by the vectors |ι|^{-1/2} gₖ ⊗ eₚ.

Equations

• τ.ampl = MIPRE.VecTrace.ofFintype τ.amplVec ⋯ ⋯ ⋯

The players' operators of an extension

theorem MIPRE.liftLeft_map {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {f : R → S} (hf : f 0 = 0) (X : Matrix α α R) : (liftLeft X).map f = liftLeft (X.map f)

The first register's matrices commute with a map of the entries vanishing at zero.

theorem MIPRE.liftRight_map {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {f : R → S} (hf : f 0 = 0) (Y : Matrix β β R) : (liftRight Y).map f = liftRight (Y.map f)

The second register's matrices commute with a map of the entries vanishing at zero.

theorem MIPRE.BipartiteModel.IsFinitePair.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsFinitePair) : M.swap.IsFinitePair

A finite pair with the players exchanged is a finite pair.

theorem MIPRE.BipartiteModel.expand_π_πA_eq_toCLM {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (M : BipartiteModel 𝒞 𝒜 ℬ) (e : α × β → ℂ) (X : Matrix α α 𝒜) : (M.expand e).π ((M.expand e).πA X) = OperatorMatrix.toCLM (liftLeft (X.map ⇑(M.π.comp M.πA)))

The first player's operators of an extension are X ⊗ 1_β over the model's operators.

theorem MIPRE.BipartiteModel.expand_π_πB_eq_toCLM {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (M : BipartiteModel 𝒞 𝒜 ℬ) (e : α × β → ℂ) (Y : Matrix β β ℬ) : (M.expand e).π ((M.expand e).πB Y) = OperatorMatrix.toCLM (liftRight (Y.map ⇑(M.π.comp M.πB)))

The second player's operators of an extension are 1_α ⊗ Y over the model's operators.

theorem MIPRE.BipartiteModel.opsA_expand_subset {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (M : BipartiteModel 𝒞 𝒜 ℬ) (e : α × β → ℂ) : (M.expand e).opsA ⊆ OperatorMatrix.toCLM '' M.opsA.matrix

The first player's operators of an extension are operators of matrices over the first player's operators of the model.

theorem MIPRE.BipartiteModel.opsB_expand_subset {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (M : BipartiteModel 𝒞 𝒜 ℬ) (e : α × β → ℂ) : (M.expand e).opsB ⊆ OperatorMatrix.toCLM '' M.opsB.matrix

The second player's operators of an extension are operators of matrices over the second player's operators of the model.

theorem MIPRE.BipartiteModel.IsFinitePair.expand {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsFinitePair) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] (e : α × β → ℂ) : (M.expand e).IsFinitePair

An ancilla extension of a finite pair is a finite pair (lem:finite-pair-expand), for nonempty registers.