A bipartite model over a given second player's algebra

Each Alice stage of introspection adjoins to the first player an ancilla register whose size is chosen along the way, by the Kraus–Halmos dilation (exists_pvm_dilation_ge). This changes the first player's algebra, and the algebra the model represents, from one stage to the next, and leaves the second player's algebra alone; a stage therefore returns a model together with its algebras. ModelOver ℬ packs a bipartite model whose second player's algebra is ℬ with its represented algebra and its first player's algebra, and the instances register measurements need (StarModule ℂ, and an ordered, proper ⋆-ring). Its ancilla extension ModelOver.expandA reduces to it (BipartiteModel.povmReduces_expandA), so a value model dominating the model at one stage dominates it at every later one.

Phase 4 of planning/mipco-track.md.

structure MIPRE.ModelOver (ℬ : Type u) [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] : Type (max (u + 1) (v + 1))

A bipartite model over the second player's algebra ℬ, packed with its represented algebra and its first player's algebra, the latter ordered and proper.

• 𝒞 : Type u

  The algebra represented on the Hilbert space.

• 𝒜 : Type u

  The first player's algebra.

• ring𝒞 : Ring self.𝒞
• starRing𝒞 : StarRing self.𝒞
• algebra𝒞 : Algebra ℂ self.𝒞
• ring𝒜 : Ring self.𝒜
• starRing𝒜 : StarRing self.𝒜
• algebra𝒜 : Algebra ℂ self.𝒜
• starModule𝒜 : StarModule ℂ self.𝒜
• partialOrder𝒜 : PartialOrder self.𝒜
• starOrderedRing𝒜 : StarOrderedRing self.𝒜
• starProper𝒜 : StarProper self.𝒜
• Ξ : BipartiteModel self.𝒞 self.𝒜 ℬ

  The model.

def MIPRE.ModelOver.of {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {𝒞 𝒜 : Type u} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) : ModelOver ℬ

A bipartite model, packed.

Equations

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

@[simp]

theorem MIPRE.ModelOver.of_Ξ {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {𝒞 𝒜 : Type u} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) : (of Ξ).Ξ = Ξ

noncomputable def MIPRE.ModelOver.expandA {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type} [Fintype T] [DecidableEq T] (N : ModelOver ℬ) (t₀ : T) : ModelOver ℬ

The first player's ancilla extension: the register T adjoined to the first player, in its reference state t₀.

Equations

• N.expandA t₀ = MIPRE.ModelOver.of (N.Ξ.expandA t₀)

@[simp]

theorem MIPRE.ModelOver.expandA_Ξ {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type} [Fintype T] [DecidableEq T] (N : ModelOver ℬ) (t₀ : T) : (N.expandA t₀).Ξ = N.Ξ.expandA t₀

theorem MIPRE.ModelOver.norm_expandA_ψ {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type} [Fintype T] [DecidableEq T] (N : ModelOver ℬ) (t₀ : T) : ‖(N.expandA t₀).Ξ.ψ‖ = ‖N.Ξ.ψ‖

theorem MIPRE.ModelOver.povmReduces_expandA {ℬ : Type u} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type} [Fintype T] [DecidableEq T] [PartialOrder ℬ] [StarOrderedRing ℬ] (N : ModelOver ℬ) (t₀ : T) : (N.expandA t₀).Ξ.POVMReduces N.Ξ

The extension reduces to the model, whatever the second player's order.