The ancilla extension of a bipartite model

A finite ancilla adjoined to a bipartite model: a register α for the first player and a register β for the second, in a joint state e : α × β → ℂ. The Hilbert space becomes H ⊗ ℂ^{α × β}, the ℓ² sum OperatorMatrix.Ampl (α × β) H of ι → H of Phase 1(a); the first player's algebra becomes the α × α matrices over 𝒜, acting as X ⊗ 1_β, and the second's the β × β matrices over ℬ, acting as 1_α ⊗ Y (BipartiteModel.expand). These are the finite ancillas of planning/mipco-track.md §5, and the expanded state of the Pauli appendix (def:expanded-state) in any model.

An element X of a player's algebra tensored with a matrix P of scalars on the register is the matrix smulKron X P with entries P a b • X. Three facts carry every use of the construction.

• The Born probability of a measurement of product form factorizes into the model's and the ancilla's (bornProb_expand_smulKron), as soon as the ancilla's two operators are positive, which makes the ancilla's quadratic form real.
• So an operator with an inert ancilla, X ⊗ 1, has the state norm it had before the expansion, scaled by the norm of e (stateSqNorm_expand_smulKron_one); and the norm of the state is the product of the norms (norm_expand_state).
• A product of projective measurements is projective (IsPVMIn.smulKron).

The matrix expanded state expVec of MIPRE/Foundations/Expanded.lean is this construction at the tensor-product model, through the bridge bornProb_expVec_eq there.

An element tensored with a matrix of scalars

def MIPRE.smulKron {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X : R) (P : Matrix α α ℂ) : Matrix α α R

X ⊗ P as an α × α matrix over R: the entry (a, b) is P a b • X.

Equations

• MIPRE.smulKron X P = P.map fun (x : ℂ) => x • X

@[simp]

theorem MIPRE.smulKron_apply {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X : R) (P : Matrix α α ℂ) (a b : α) : smulKron X P a b = P a b • X

theorem MIPRE.smulKron_zero_left {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (P : Matrix α α ℂ) : smulKron 0 P = 0

theorem MIPRE.smulKron_zero_right {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X : R) : smulKron X 0 = 0

theorem MIPRE.smulKron_sum_left {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] {ι : Type u_3} (s : Finset ι) (X : ι → R) (P : Matrix α α ℂ) : smulKron (∑ i ∈ s, X i) P = ∑ i ∈ s, smulKron (X i) P

theorem MIPRE.smulKron_sum_right {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] {ι : Type u_3} (X : R) (s : Finset ι) (P : ι → Matrix α α ℂ) : smulKron X (∑ i ∈ s, P i) = ∑ i ∈ s, smulKron X (P i)

theorem MIPRE.star_smulKron {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [StarRing R] [StarModule ℂ R] (X : R) (P : Matrix α α ℂ) : star (smulKron X P) = smulKron (star X) P.conjTranspose

The adjoint of X ⊗ P is X* ⊗ P*.

theorem MIPRE.smulKron_mul {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [Fintype α] (X Y : R) (P Q : Matrix α α ℂ) : smulKron X P * smulKron Y Q = smulKron (X * Y) (P * Q)

theorem MIPRE.smulKron_add_left {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X Y : R) (P : Matrix α α ℂ) : smulKron (X + Y) P = smulKron X P + smulKron Y P

theorem MIPRE.smulKron_sub_left {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X Y : R) (P : Matrix α α ℂ) : smulKron X P - smulKron Y P = smulKron (X - Y) P

theorem MIPRE.smulKron_add_right {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X : R) (P Q : Matrix α α ℂ) : smulKron X (P + Q) = smulKron X P + smulKron X Q

theorem MIPRE.smulKron_smul_right {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] (X : R) (c : ℂ) (P : Matrix α α ℂ) : smulKron X (c • P) = c • smulKron X P

theorem MIPRE.smulKron_one_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [DecidableEq α] : smulKron 1 1 = 1

theorem MIPRE.star_smulKron_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [DecidableEq α] [StarRing R] (X : R) : star (smulKron X 1) = smulKron (star X) 1

The adjoint of X ⊗ 1 is X* ⊗ 1, in any ⋆-ring.

theorem MIPRE.smulKron_nonneg_of_proj {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [Fintype α] [StarRing R] [StarModule ℂ R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {X : R} (hX : 0 ≤ X) {P : Matrix α α ℂ} (hP : P.conjTranspose * P = P) : 0 ≤ smulKron X P

A nonnegative element times a projection of the register is nonnegative, in the order of the matrices over a proper ordered ⋆-ring (MIPRE.MatrixStar.instPartialOrderStar): z⋆ z ⊗ P = (z ⊗ P)⋆ (z ⊗ P) when Pᴴ P = P.

theorem MIPRE.IsPVMIn.smulKron {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [DecidableEq α] [Fintype α] [StarRing R] [StarModule ℂ R] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] {P : ι → R} {Q : κ → Matrix α α ℂ} (hP : IsPVMIn P) (hQ : IsPVMIn Q) : IsPVMIn fun (p : ι × κ) => MIPRE.smulKron (P p.1) (Q p.2)

A product of projective measurements is projective: the first in R, the second of scalar matrices on the register.

theorem MIPRE.IsPVMIn.smulKron_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [DecidableEq α] [Fintype α] [StarRing R] [StarModule ℂ R] {ι : Type u_3} [Fintype ι] {P : ι → Matrix α α ℂ} (hP : IsPVMIn P) : IsPVMIn fun (i : ι) => MIPRE.smulKron 1 (P i)

A projective measurement of the register is projective in the matrices over R, as P ↦ 1 ⊗ P.

The two registers of a pair

def MIPRE.liftLeft {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] : Matrix α α R →⋆ₐ[ℂ] Matrix (α × β) (α × β) R

The first register's matrices acting on the pair of registers, X ↦ X ⊗ 1_β.

Equations

• MIPRE.liftLeft = { toFun := fun (X : Matrix α α R) => Matrix.blockDiagonal fun (x : β) => X, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

theorem MIPRE.liftLeft_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (X : Matrix α α R) (p q : α × β) : liftLeft X p q = if p.2 = q.2 then X p.1 q.1 else 0

def MIPRE.liftRight {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] : Matrix β β R →⋆ₐ[ℂ] Matrix (α × β) (α × β) R

The second register's matrices acting on the pair of registers, Y ↦ 1_α ⊗ Y: the first register's lift with the two registers exchanged.

Equations

• MIPRE.liftRight = { toAlgHom := (↑(Matrix.reindexAlgEquiv ℂ R (Equiv.prodComm β α))).comp ↑MIPRE.liftLeft, map_star' := ⋯ }

theorem MIPRE.liftRight_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Y : Matrix β β R) (p q : α × β) : liftRight Y p q = if p.1 = q.1 then Y p.2 q.2 else 0

theorem MIPRE.liftLeft_mul_liftRight {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (X : Matrix α α R) (Y : Matrix β β R) (p q : α × β) : (liftLeft X * liftRight Y) p q = X p.1 q.1 * Y p.2 q.2

The two registers' matrices multiply entrywise.

theorem MIPRE.liftRight_mul_liftLeft {R : Type u_1} {α : Type u_2} {β : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (X : Matrix α α R) (Y : Matrix β β R) (p q : α × β) : (liftRight Y * liftLeft X) p q = Y p.2 q.2 * X p.1 q.1

def MIPRE.mapMatrixStarAlgHom {A : Type u_1} {B : Type u_2} {n : Type u_3} [Fintype n] [DecidableEq n] [Ring A] [StarRing A] [Algebra ℂ A] [Ring B] [StarRing B] [Algebra ℂ B] (f : A →⋆ₐ[ℂ] B) : Matrix n n A →⋆ₐ[ℂ] Matrix n n B

A ⋆-algebra homomorphism, applied entrywise to square matrices.

Equations

• MIPRE.mapMatrixStarAlgHom f = { toAlgHom := (↑f).mapMatrix, map_star' := ⋯ }

@[simp]

theorem MIPRE.mapMatrixStarAlgHom_apply {A : Type u_1} {B : Type u_2} {n : Type u_3} [Fintype n] [DecidableEq n] [Ring A] [StarRing A] [Algebra ℂ A] [Ring B] [StarRing B] [Algebra ℂ B] (f : A →⋆ₐ[ℂ] B) (X : Matrix n n A) : (mapMatrixStarAlgHom f) X = X.map ⇑f

theorem MIPRE.StateModel.qform_one_eq_norm_sq {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) : M.qform 1 = ‖M.ψ‖ ^ 2

The quadratic form of the identity is the squared norm of the state.

The extension

noncomputable def MIPRE.BipartiteModel.expand {𝒞 : 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 : α × β → ℂ) : BipartiteModel (Matrix (α × β) (α × β) 𝒞) (Matrix α α 𝒜) (Matrix β β ℬ)

The ancilla extension of a bipartite model by a register α for the first player and a register β for the second, in the joint state e: the space H ⊗ ℂ^{α × β}, the state ψ ⊗ e, the first player's α × α matrices over 𝒜 acting as X ⊗ 1_β and the second's β × β matrices over ℬ acting as 1_α ⊗ Y.

Equations

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

theorem MIPRE.BipartiteModel.expand_ψ {𝒞 : 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).ψ = WithLp.toLp 2 fun (p : α × β) => e p • M.ψ

theorem MIPRE.BipartiteModel.expand_π_apply {𝒞 : 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 : α × β → ℂ) (Z : Matrix (α × β) (α × β) 𝒞) : (M.expand e).π Z = OperatorMatrix.toCLM (Z.map ⇑M.π)

theorem MIPRE.BipartiteModel.expand_πA_smulKron {𝒞 : 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 : 𝒜) (P : Matrix α α ℂ) : (M.expand e).πA (smulKron X P) = liftLeft (smulKron (M.πA X) P)

theorem MIPRE.BipartiteModel.expand_πB_smulKron {𝒞 : 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 : ℬ) (Q : Matrix β β ℂ) : (M.expand e).πB (smulKron Y Q) = liftRight (smulKron (M.πB Y) Q)

theorem MIPRE.BipartiteModel.toCLM_liftLeft_mul_liftRight_smulKron {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : 𝒞 →⋆ₐ[ℂ] H →L[ℂ] H) (a b : 𝒞) (P : Matrix α α ℂ) (Q : Matrix β β ℂ) (ξ : H) : (OperatorMatrix.toCLM ((liftLeft (smulKron a P) * liftRight (smulKron b Q)).map ⇑π)) (WithLp.toLp 2 fun (p : α × β) => e p • ξ) = WithLp.toLp 2 fun (p : α × β) => (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q).mulVec e p • (π (a * b)) ξ

The action of a product operator on a product vector of the amplified space: entrywise, the model's operator on the model's vector and the scalar Kronecker product on the ancilla's.

theorem MIPRE.BipartiteModel.inner_toLp_smul {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α × β → ℂ) {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (c : α × β → ℂ) (ξ η : H) : inner ℂ (WithLp.toLp 2 fun (p : α × β) => e p • ξ) (WithLp.toLp 2 fun (p : α × β) => c p • η) = star e ⬝ᵥ c * inner ℂ ξ η

The inner product of two product vectors of the amplified space.

theorem MIPRE.BipartiteModel.expand_π_smulKron_ψ {𝒞 : 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 : 𝒜) (Y : ℬ) (P : Matrix α α ℂ) (Q : Matrix β β ℂ) : ((M.expand e).π ((M.expand e).πA (smulKron X P) * (M.expand e).πB (smulKron Y Q))) (M.expand e).ψ = WithLp.toLp 2 fun (p : α × β) => (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q).mulVec e p • (M.π (M.πA X * M.πB Y)) M.ψ

An operator of product form acts on the extended state factor by factor: on the model's state as the model's operator, and on the ancilla's as the Kronecker product of the two scalar matrices.

theorem MIPRE.BipartiteModel.inner_expand_smulKron {𝒞 : 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 : 𝒜) (Y : ℬ) (P : Matrix α α ℂ) (Q : Matrix β β ℂ) : inner ℂ (M.expand e).ψ (((M.expand e).π ((M.expand e).πA (smulKron X P) * (M.expand e).πB (smulKron Y Q))) (M.expand e).ψ) = star e ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q).mulVec e * inner ℂ M.ψ ((M.π (M.πA X * M.πB Y)) M.ψ)

The quadratic form of a product operator on the extended state, before real parts.

theorem MIPRE.BipartiteModel.bornProb_expand_smulKron_eq {𝒞 : 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 : 𝒜) (Y : ℬ) (P : Matrix α α ℂ) (Q : Matrix β β ℂ) : (M.expand e).bornProb (smulKron X P) (smulKron Y Q) = (star e ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q).mulVec e * inner ℂ M.ψ ((M.π (M.πA X * M.πB Y)) M.ψ)).re

The Born probability of a product measurement on the extended state, before the ancilla's factor is known to be real.

theorem MIPRE.BipartiteModel.bornProb_expand_smulKron {𝒞 : 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 : 𝒜) (Y : ℬ) {P : Matrix α α ℂ} {Q : Matrix β β ℂ} (hP : P.PosSemidef) (hQ : Q.PosSemidef) : (M.expand e).bornProb (smulKron X P) (smulKron Y Q) = MIPRE.bornProb e P Q * M.bornProb X Y

The Born probability of a product measurement on the extended state factorizes: the model's Born probability times the ancilla's. Only the ancilla's two operators need to be positive: that is what makes their quadratic form real, which is what lets the real part of the product split.

theorem MIPRE.BipartiteModel.stateSqNorm_eq_bornProb_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : N.stateSqNorm a = N.bornProb (star a * a) 1

The model's Born probability against the identity is its first player's squared norm.

theorem MIPRE.BipartiteModel.stateSqNorm_expand_smulKron_one {𝒞 : 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 : 𝒜) : (M.expand e).stateSqNorm (smulKron X 1) = ‖evec e‖ ^ 2 * M.stateSqNorm X

An inert ancilla changes nothing: the first player's operator X ⊗ 1 has, on the extended state, the squared norm ‖e‖² times the one X has on the model's state.

theorem MIPRE.BipartiteModel.swap_stateSqNorm_expand_smulKron_one {𝒞 : 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 : ℬ) : (M.expand e).swap.stateSqNorm (smulKron Y 1) = ‖evec e‖ ^ 2 * M.swap.stateSqNorm Y

The same for the second player.

theorem MIPRE.BipartiteModel.norm_expand_state {𝒞 : 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).ψ‖ = ‖evec e‖ * ‖M.ψ‖

The norm of the extended state is the product of the norms.