The symmetric model: the state, the placements and the swap symmetry

This is the base file of the port of the vendored low-individual-degree test (MIPRE/Background/LIDT/MIPStarRE/LDT/) from finite-dimensional matrices to a vector state on a Hilbert space (planning/c6b-plan.md, milestone M0, and its section "Port conventions"). It is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/QuantumState.lean.

The vendored development works with a density matrix ψ on ι × ι, places a local operator A : Op ι on the two tensor factors as leftTensor A = A ⊗ 1 and rightTensor A = 1 ⊗ A, and assumes, for its symmetric strategies, that ψ is fixed by the swap of the two factors. Here a symmetric model SymModel 𝔓 K is

• a C*-algebra 𝔓 of local operators (the vendored Op ι), with its order;
• a Hilbert space K and a unit vector Ψ ∈ K (the state);
• a ⋆-homomorphism L : 𝔓 →⋆ₐ[ℂ] (K →L[ℂ] K), the first player's placement (leftTensor);
• a self-inverse isometry J of K fixing Ψ, whose conjugation flip carries L to the second player's placement R := flip ∘ L (rightTensor), and such that the two placements commute.

Joint operators (the vendored Op (ι × ι)) are elements of K →L[ℂ] K, and the expectation is ev X = Re ⟪Ψ, X Ψ⟫ = Op.qform Ψ X (MIPRE/Foundations/OpCalculus.lean), so the linearity, monotonicity and positivity of the vendored ev are those of Op.qform.

The vendored swap symmetry (PermInvState, swapDensity, the *_of_density_fixed lemmas of LDT/Test/StrategyCore.lean) is a hypothesis on a strategy there; here it is three theorems of the structure (reports/c6b-paper-proofs.md, §4.1 and Theorem B):

• ev_flip : ev (flip X) = ev X, since J fixes Ψ;
• ev_L_eq_ev_R : ev (L x) = ev (R x), the vendored PermInvState.swap_ev;
• ev_L_mul_R_comm : ev (L x * R y) = ev (L y * R x), the vendored ev_opTensor_swap_of_density_fixed.

The state alone is a vector state VecState K (the fields Ψ, Ψ_norm), the parent structure of SymModel. Everything that uses only the state, and not the placements or the flip, is a VecState declaration: ev and its linear and positivity lemmas here, and downstream the same-space defects and relations (qSDD, sddError, SDDRel, …, Co/Test/Defs.lean). They apply to a state with no swap symmetry (the vendored QuantumState ι on one space, the reduced or tensored states of MakingMeasurementsProjective), and are reached from S : SymModel 𝔓 K by the same dot notation, S.ev X being S.toVecState.ev X; an explicit argument (V : VecState K) accepts S through a coercion.

The vector state is a state model of the repository (VecState.toStateModel, with H := K, π := id), and the symmetric model a bipartite model (toBipartite, with in addition πA := L, πB := R), so the state calculus of MIPRE/Foundations/ applies to both unchanged.

Every positivity lemma on the joint operators K →L[ℂ] K is proved here, in a file that imports only Foundations and the Mathlib they import, and is applied downstream: positivity on K →L[ℂ] K is the expensive part of elaboration, and it roughly doubles under the wholesale import Mathlib of the vendored classical layer (planning/c6b-plan.md, §5). Positivity in the local algebra 𝔓, or in a generic ordered ⋆-ring, stays with its vendored file.

Translation

QuantumState (ι × ι) ψ ↦ S : SymModel 𝔓 K; ev ψ X ↦ S.ev X; leftTensor A ↦ S.L A; rightTensor A ↦ S.R A; opTensor A B ↦ S.opTensor A B = S.L A * S.R B; ᴴ ↦ star; swapDensity ↦ S.flip; a state on one space ↦ V : VecState K. Lemmas keep their vendored names, as SymModel lemmas (S.leftTensor_mul_leftTensor, stated with S.L) or, when they use only the state, VecState lemmas (S.ev_add, V.ev_add).

New here

• VecState, VecState.toStateModel (with toStateModel_qform, toStateModel_snorm), the coercion of a SymModel to its VecState;
• the flip and its lemmas (flip, R_apply, J_symm, flip_apply, flip_flip, flip_L, flip_R, L_comm_R), the swap symmetry (ev_flip, ev_L_eq_ev_R, ev_L_mul_R_comm);
• toBipartite and its simp lemmas;
• leftTensor_real_smul, rightTensor_real_smul: placement of a real scalar multiple;
• opTensor_le_one: a product placement of two effects is an effect.

Ported here from other vendored files

So that every positivity proof sits in this file, the following are ported here rather than in the counterparts of their vendored files: from LDT/Basic/OperatorExpectations.lean, ev_add, ev_sub, ev_scale, ev_real_smul, ev_zero, ev_opTensor, ev_one_of_isNormalized, ev_adjoint_self_nonneg, ev_finset_sum, ev_sum, ev_nonneg_of_psd, ev_mono, ev_conjTranspose, ev_mul_comm_of_hermitian, ev_mul_comm_of_psd, ev_conjTranspose_mul_comm; from LDT/Basic/TensorPlacement.lean, leftTensor_finset_sum, rightTensor_finset_sum, leftTensor_nonneg, rightTensor_nonneg, leftTensor_le_one, rightTensor_le_one; from LDT/Test/StrategyCore.lean, swapDensity_opTensor, ev_swapDensity_of_density_fixed, ev_opTensor_swap_of_density_fixed; from Quantum/FiniteMatrix/Order.lean, sq_le_self (for any C*-algebra).

Not ported

Matrix-only or density-only declarations of the vendored file, each replaced by the model:

• QuantumState: replaced by VecState (a state on one space) and SymModel (a symmetric state on two); the state is the vector Ψ, not a density matrix.
• QuantumState.IsNormalized.nonempty: supplies Nonempty ι to the normalized trace, which the model does not have; K contains the unit vector Ψ.
• pureDensity: the scaled rank-one density of a vector; the state is a vector here.
• swapVector: replaced by the field J.
• swapVector_swapVector: replaced by the field J_J.
• PureState: the state is a unit vector already (Ψ, Ψ_norm).
• PureState.basis_unit: a coordinate vector of ι → ℂ; no coordinates here.
• PureState.basis: a coordinate vector of ι → ℂ; no coordinates here.
• PureState.density: density of a vector; no density here.
• PureState.density_psd: density of a vector; no density here.
• PureState.toQuantumState: the coercion of a vector to a density; no density here.
• PureState.coe_density: the coercion of a vector to a density; no density here.
• PureState.normalizedTrace_density: normalized trace; replaced by Ψ_norm and ev_one_of_isNormalized.
• PureState.toQuantumState_isNormalized: replaced by isNormalized.
• PureState.normalizedTrace_density_mul: normalized trace of ρ X; replaced by ev_eq_re_inner, which holds by definition.
• PureState.IsSwapInvariant: replaced by the field J_Ψ.
• leftTensor: replaced by the field L.
• rightTensor: replaced by R.
• normalizedTrace_opTensor: the model has no trace.
• QuantumState.tensor: the tensor product of two states; the model has one state and no tensor product of Hilbert spaces.
• QuantumState.tensor_density: as QuantumState.tensor.
• QuantumState.tensor_isNormalized: as QuantumState.tensor.

structure MIPRE.LIDT.Co.VecState (K : Type u_1) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : Type u_1

A vector state: a unit vector Ψ in a Hilbert space K, acting on the operators of K by X ↦ Re ⟪Ψ, X Ψ⟫. It is the vendored QuantumState ι of a state on one space, as a vector state; it is the parent of SymModel, and the same-space quantities of the port (ev, qSDD, SDDRel, …) are VecState declarations, reached from S : SymModel 𝔓 K by the same dot notation (S.ev X is S.toVecState.ev X).

• Ψ : K

  The state.

• Ψ_norm : ‖self.Ψ‖ = 1

  The state is a unit vector (the vendored QuantumState.IsNormalized).

structure MIPRE.LIDT.Co.SymModel (𝔓 : Type u_1) [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (K : Type u_2) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] extends MIPRE.LIDT.Co.VecState K : Type (max u_1 u_2)

A symmetric model: a vector state Ψ in a Hilbert space K, a ⋆-homomorphism L from a C*-algebra 𝔓 of local operators into the operators on K (the first player's placement), and a self-inverse isometry J of K fixing Ψ whose conjugation carries L to an operator family commuting with L (the second player's placement R).

• Ψ : K
• Ψ_norm : ‖self.Ψ‖ = 1
• L : 𝔓 →⋆ₐ[ℂ] K →L[ℂ] K

  The first player's placement (the vendored leftTensor).

• J : K ≃ₗᵢ[ℂ] K

  The flip of the two players (the vendored swapVector).

• J_J (v : K) : self.J (self.J v) = v

  The flip is an involution.

• J_Ψ : self.J self.Ψ = self.Ψ

  The state is symmetric (the vendored PureState.IsSwapInvariant).

• commute (x y : 𝔓) : Commute (self.L x) (self.J.conjStarAlgEquiv (self.L y))

  The two placements commute.

theorem MIPRE.LIDT.Co.sq_le_self {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {X : A} (hX : 0 ≤ X) (hXle : X ≤ 1) : X * X ≤ X

An operator between 0 and 1 dominates its square: X (1 - X) is a product of commuting positive elements.

The expectation

noncomputable def MIPRE.LIDT.Co.VecState.ev {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : ℝ

The expectation Re ⟪Ψ, X Ψ⟫ of a joint operator (the vendored ev ψ X = Re τ(ρ X)).

Equations

• V.ev X = MIPRE.Op.qform V.Ψ X

theorem MIPRE.LIDT.Co.VecState.ev_eq_re_inner {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : V.ev X = (inner ℂ V.Ψ (X V.Ψ)).re

The expectation is the real part of the inner product (the vendored PureState.ev_eq_re_inner).

theorem MIPRE.LIDT.Co.VecState.ev_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y : K →L[ℂ] K) : V.ev (X + Y) = V.ev X + V.ev Y

ev distributes over addition.

theorem MIPRE.LIDT.Co.VecState.ev_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y : K →L[ℂ] K) : V.ev (X - Y) = V.ev X - V.ev Y

ev distributes over subtraction.

theorem MIPRE.LIDT.Co.VecState.ev_scale {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (c : ℝ) (X : K →L[ℂ] K) : V.ev (↑c • X) = c * V.ev X

ev commutes with complex scalar multiplication by a real number.

theorem MIPRE.LIDT.Co.VecState.ev_real_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (c : ℝ) (X : K →L[ℂ] K) : V.ev (c • X) = c * V.ev X

ev commutes with the real scalar action on operators.

theorem MIPRE.LIDT.Co.VecState.ev_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) : V.ev 0 = 0

ev of the zero operator is zero.

theorem MIPRE.LIDT.Co.VecState.ev_finset_sum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {α : Type u_2} (s : Finset α) (f : α → K →L[ℂ] K) : V.ev (∑ a ∈ s, f a) = ∑ a ∈ s, V.ev (f a)

ev distributes over finite sums.

theorem MIPRE.LIDT.Co.VecState.ev_sum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {α : Type u_2} [Fintype α] (f : α → K →L[ℂ] K) : V.ev (∑ a : α, f a) = ∑ a : α, V.ev (f a)

ev distributes over univ sums.

def MIPRE.LIDT.Co.VecState.IsNormalized {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) : Prop

The state has unit expectation on the identity (the vendored QuantumState.IsNormalized, τ(ρ) = 1).

Equations

• V.IsNormalized = (V.ev 1 = 1)

@[simp]

theorem MIPRE.LIDT.Co.VecState.ev_one_of_isNormalized {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) : V.ev 1 = 1

A normalized state has unit expectation on the identity operator.

theorem MIPRE.LIDT.Co.VecState.isNormalized {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) : V.IsNormalized

A vector state is normalized.

theorem MIPRE.LIDT.Co.VecState.ev_nonneg_of_psd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) (hX : 0 ≤ X) : 0 ≤ V.ev X

ev of a positive operator is nonnegative.

theorem MIPRE.LIDT.Co.VecState.ev_mono {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y : K →L[ℂ] K) (h : X ≤ Y) : V.ev X ≤ V.ev Y

ev is monotone.

theorem MIPRE.LIDT.Co.VecState.ev_adjoint_self_eq_norm_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (M : K →L[ℂ] K) : V.ev (star M * M) = ‖M V.Ψ‖ ^ 2

ev (M* M) = ‖M Ψ‖².

theorem MIPRE.LIDT.Co.VecState.ev_adjoint_self_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (M : K →L[ℂ] K) : 0 ≤ V.ev (star M * M)

For any operator M, ev (M* M) ≥ 0.

noncomputable def MIPRE.LIDT.Co.VecState.toStateModel {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) : StateModel (K →L[ℂ] K)

The vector state as a state model of the repository (MIPRE/Foundations/StateModel.lean): H := K, ψ := Ψ, π := id. Its quadratic form is ev and its state norm ‖X Ψ‖, both by rfl.

Equations

• V.toStateModel = { H := K, normedAddCommGroup := inst✝², innerProductSpace := inst✝¹, completeSpace := inst✝, ψ := V.Ψ, π := StarAlgHom.id ℂ (K →L[ℂ] K) }

theorem MIPRE.LIDT.Co.VecState.toStateModel_qform {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : V.toStateModel.qform X = V.ev X

The quadratic form of the state model is ev.

theorem MIPRE.LIDT.Co.VecState.toStateModel_snorm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : V.toStateModel.snorm X = ‖X V.Ψ‖

The state norm of the state model is ‖X Ψ‖.

theorem MIPRE.LIDT.Co.VecState.ev_conjTranspose {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : V.ev (star X) = V.ev X

Taking the adjoint does not change ev.

theorem MIPRE.LIDT.Co.VecState.ev_mul_comm_of_hermitian {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) (hA : star A = A) (hB : star B = B) : V.ev (A * B) = V.ev (B * A)

ev (A B) = ev (B A) for self-adjoint A and B.

theorem MIPRE.LIDT.Co.VecState.ev_mul_comm_of_psd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) (hA : 0 ≤ A) (hB : 0 ≤ B) : V.ev (A * B) = V.ev (B * A)

ev commutes on positive operators.

theorem MIPRE.LIDT.Co.VecState.ev_conjTranspose_mul_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : V.ev (star B * A) = V.ev (star A * B)

Cross-term identity: ev (B* A) = ev (A* B).

@[instance_reducible]

instance MIPRE.LIDT.Co.SymModel.instCoeOutVecState {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : CoeOut (SymModel 𝔓 K) (VecState K)

A symmetric model is a vector state: an explicit argument (V : VecState K) accepts S : SymModel 𝔓 K.

Equations

• MIPRE.LIDT.Co.SymModel.instCoeOutVecState = { coe := MIPRE.LIDT.Co.SymModel.toVecState }

The flip and the second placement

noncomputable def MIPRE.LIDT.Co.SymModel.flip {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : (K →L[ℂ] K) ≃⋆ₐ[ℂ] K →L[ℂ] K

The flip of the joint operators, X ↦ J X J (the vendored swapDensity).

Equations

• S.flip = S.J.conjStarAlgEquiv

noncomputable def MIPRE.LIDT.Co.SymModel.R {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : 𝔓 →⋆ₐ[ℂ] K →L[ℂ] K

The second player's placement R x = J (L x) J (the vendored rightTensor).

Equations

• S.R = S.flip.toStarAlgHom.comp S.L

theorem MIPRE.LIDT.Co.SymModel.R_apply {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.R x = S.flip (S.L x)

The second placement is the flip of the first.

theorem MIPRE.LIDT.Co.SymModel.J_symm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (v : K) : S.J.symm v = S.J v

The flip is its own inverse.

theorem MIPRE.LIDT.Co.SymModel.flip_apply {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) (v : K) : (S.flip X) v = S.J (X (S.J v))

The flip of an operator, applied to a vector: (J X J) v.

theorem MIPRE.LIDT.Co.SymModel.flip_flip {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.flip (S.flip X) = X

The flip of the joint operators is an involution.

theorem MIPRE.LIDT.Co.SymModel.flip_L {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.flip (S.L x) = S.R x

The flip carries the first placement to the second.

theorem MIPRE.LIDT.Co.SymModel.flip_R {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.flip (S.R x) = S.L x

The flip carries the second placement to the first.

theorem MIPRE.LIDT.Co.SymModel.L_comm_R {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x y : 𝔓) : Commute (S.L x) (S.R y)

The two placements commute.

The model as a bipartite model

noncomputable def MIPRE.LIDT.Co.SymModel.toBipartite {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : BipartiteModel (K →L[ℂ] K) 𝔓 𝔓

The symmetric model as a bipartite model of the repository: H := K, π := id, πA := L, πB := R.

Equations

• S.toBipartite = { toStateModel := S.toStateModel, πA := S.L, πB := S.R, commute := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.SymModel.toBipartite_ψ {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : S.toBipartite.ψ = S.Ψ

The state of the bipartite model is Ψ.

theorem MIPRE.LIDT.Co.SymModel.toBipartite_ψ_norm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : ‖S.toBipartite.ψ‖ = 1

The state of the bipartite model is a unit vector.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.toBipartite_π {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.toBipartite.π X = X

The representation of the bipartite model is the identity.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.toBipartite_πA {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.toBipartite.πA x = S.L x

The bipartite model's first placement is L.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.toBipartite_πB {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.toBipartite.πB x = S.R x

The bipartite model's second placement is R.

theorem MIPRE.LIDT.Co.SymModel.toBipartite_qform {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.toBipartite.qform X = S.ev X

The quadratic form of the bipartite model is ev.

theorem MIPRE.LIDT.Co.SymModel.toBipartite_snorm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.toBipartite.snorm X = ‖X S.Ψ‖

The state norm of the bipartite model is ‖X Ψ‖.

The swap symmetry

theorem MIPRE.LIDT.Co.SymModel.ev_flip {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.ev (S.flip X) = S.ev X

The flip fixes the state: ev (J X J) = ev X.

theorem MIPRE.LIDT.Co.SymModel.ev_L_eq_ev_R {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x : 𝔓) : S.ev (S.L x) = S.ev (S.R x)

The two placements have the same expectations (the vendored PermInvState.swap_ev).

theorem MIPRE.LIDT.Co.SymModel.ev_L_mul_R_comm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (x y : 𝔓) : S.ev (S.L x * S.R y) = S.ev (S.L y * S.R x)

The expectation of a product placement is symmetric (the vendored ev_opTensor_swap_of_density_fixed).

theorem MIPRE.LIDT.Co.SymModel.ev_swapDensity_of_density_fixed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (Z : K →L[ℂ] K) : S.ev (S.flip Z) = S.ev Z

The flip preserves ev (the vendored ev_swapDensity_of_density_fixed, where the fixed density was a hypothesis).

Tensor placement

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.SymModel.opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : K →L[ℂ] K

The product placement A ⊗ B = L A * R B (the vendored Kronecker product).

Equations

• S.opTensor A B = S.L A * S.R B

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.ev (S.opTensor A B) = S.ev (S.L A * S.R B)

Expectation of a tensor product can be written using left/right placements.

theorem MIPRE.LIDT.Co.SymModel.swapDensity_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y : 𝔓) : S.flip (S.opTensor X Y) = S.opTensor Y X

The flip exchanges the factors of a product placement.

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_swap_of_density_fixed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y : 𝔓) : S.ev (S.opTensor X Y) = S.ev (S.opTensor Y X)

The expectation of a product placement is symmetric in its factors.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : S.L 1 = 1

Left placement of the identity is the identity.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) : S.R 1 = 1

Right placement of the identity is the identity.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_rightTensor_eq_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.L A * S.R B = S.opTensor A B

Local placements multiply to the product placement.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_mul_leftTensor_eq_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.R B * S.L A = S.opTensor A B

R B * L A = A ⊗ B.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_leftTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.L A * S.L B = S.L (A * B)

L A * L B = L (A * B).

theorem MIPRE.LIDT.Co.SymModel.rightTensor_mul_rightTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.R A * S.R B = S.R (A * B)

R A * R B = R (A * B).

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.L A * S.opTensor B C = S.opTensor (A * B) C

Multiplying a left placement into a product placement only affects the left factor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_mul_leftTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.opTensor A C * S.L B = S.opTensor (A * B) C

Multiplying a product placement by a left placement only affects the left factor.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_mul_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.R A * S.opTensor B C = S.opTensor B (A * C)

Multiplying a right placement into a product placement only affects the right factor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_mul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A₁ A₂ B₁ B₂ : 𝔓) : S.opTensor A₁ B₁ * S.opTensor A₂ B₂ = S.opTensor (A₁ * A₂) (B₁ * B₂)

Product placements multiply factorwise.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_smul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℂ) (A : 𝔓) : c • S.L A = S.L (c • A)

Scalar multiplication commutes with left placement.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.leftTensor_real_smul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A : 𝔓) : S.L (c • A) = c • S.L A

Left placement commutes with real scalar multiplication. Mathlib's map_smul does not apply to a real scalar on a ℂ-algebra homomorphism, so a simp call meeting S.L (c • A) with c : ℝ needs this lemma.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.rightTensor_real_smul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A : 𝔓) : S.R (c • A) = c • S.R A

Right placement commutes with real scalar multiplication (as leftTensor_real_smul).

theorem MIPRE.LIDT.Co.SymModel.leftTensor_pow {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A : 𝔓) (n : ℕ) : S.L A ^ n = S.L (A ^ n)

Powers commute with left placement.

theorem MIPRE.LIDT.Co.SymModel.conjTranspose_opTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : star (S.opTensor A B) = S.opTensor (star A) (star B)

The adjoint distributes over a product placement.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_conjTranspose {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A : 𝔓) : star (S.L A) = S.L (star A)

The adjoint commutes with left placement. (The vendored @[simp] is dropped: it would loop with map_star.)

theorem MIPRE.LIDT.Co.SymModel.rightTensor_conjTranspose {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (B : 𝔓) : star (S.R B) = S.R (star B)

The adjoint commutes with right placement.

theorem MIPRE.LIDT.Co.SymModel.opTensor_sub_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.opTensor A C - S.opTensor B C = S.opTensor (A - B) C

opTensor is linear in the left factor: subtraction.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_sub {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.L A - S.L B = S.L (A - B)

Left placement commutes with subtraction.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_sub {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : 𝔓) : S.R A - S.R B = S.R (A - B)

Right placement commutes with subtraction.

theorem MIPRE.LIDT.Co.SymModel.opTensor_smul_left_error {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.opTensor (c • A) B = c • S.opTensor A B

opTensor is linear in the left factor: real scalar multiplication.

theorem MIPRE.LIDT.Co.SymModel.opTensor_smul_right_error {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.opTensor A (c • B) = c • S.opTensor A B

opTensor is linear in the right factor: real scalar multiplication.

theorem MIPRE.LIDT.Co.SymModel.opTensor_add_left_local {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.opTensor (A + B) C = S.opTensor A C + S.opTensor B C

opTensor is additive in the left factor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_add_right_local {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B C : 𝔓) : S.opTensor A (B + C) = S.opTensor A B + S.opTensor A C

opTensor is additive in the right factor.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_finset_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (s : Finset α) (f : α → 𝔓) : ∑ a ∈ s, S.L (f a) = S.L (∑ a ∈ s, f a)

Left placement commutes with finite sums.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_finset_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (s : Finset α) (f : α → 𝔓) : ∑ a ∈ s, S.R (f a) = S.R (∑ a ∈ s, f a)

Right placement commutes with finite sums.

theorem MIPRE.LIDT.Co.SymModel.opTensor_sum_left_finset {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (s : Finset α) (f : α → 𝔓) (B : 𝔓) : S.opTensor (∑ a ∈ s, f a) B = ∑ a ∈ s, S.opTensor (f a) B

Pull a finite sum out of the left factor of opTensor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_sum_right_finset {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (A : 𝔓) (s : Finset α) (f : α → 𝔓) : S.opTensor A (∑ a ∈ s, f a) = ∑ a ∈ s, S.opTensor A (f a)

Pull a finite sum out of the right factor of opTensor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_sum_left_univ {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (f : α → 𝔓) (B : 𝔓) : S.opTensor (∑ a : α, f a) B = ∑ a : α, S.opTensor (f a) B

Pull an unindexed finite-type sum out of the left factor of opTensor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_sum_right_univ {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : 𝔓) (f : α → 𝔓) : S.opTensor A (∑ a : α, f a) = ∑ a : α, S.opTensor A (f a)

Pull an unindexed finite-type sum out of the right factor of opTensor.

Positivity of the placements

theorem MIPRE.LIDT.Co.SymModel.leftTensor_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A : 𝔓} (hA : 0 ≤ A) : 0 ≤ S.L A

Left placement preserves positivity.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A : 𝔓} (hA : 0 ≤ A) : 0 ≤ S.R A

Right placement preserves positivity.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mono {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A₁ A₂ : 𝔓} (hA : A₁ ≤ A₂) : S.L A₁ ≤ S.L A₂

Left placement is monotone.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_mono {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {B₁ B₂ : 𝔓} (hB : B₁ ≤ B₂) : S.R B₁ ≤ S.R B₂

Right placement is monotone.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A : 𝔓} (hA : A ≤ 1) : S.L A ≤ 1

Left placement preserves the bound ≤ 1.

theorem MIPRE.LIDT.Co.SymModel.rightTensor_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A : 𝔓} (hA : A ≤ 1) : S.R A ≤ 1

Right placement preserves the bound ≤ 1.

theorem MIPRE.LIDT.Co.SymModel.opTensor_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A B : 𝔓} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ S.opTensor A B

Positivity is preserved by opTensor: a product of commuting positive operators.

theorem MIPRE.LIDT.Co.SymModel.opTensor_mono_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A₁ A₂ B : 𝔓} (hA : A₁ ≤ A₂) (hB : 0 ≤ B) : S.opTensor A₁ B ≤ S.opTensor A₂ B

opTensor is monotone in the left factor against a positive right factor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_mono_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A B₁ B₂ : 𝔓} (hA : 0 ≤ A) (hB : B₁ ≤ B₂) : S.opTensor A B₁ ≤ S.opTensor A B₂

opTensor is monotone in the right factor against a positive left factor.

theorem MIPRE.LIDT.Co.SymModel.opTensor_le_leftTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A B : 𝔓} (hA : 0 ≤ A) (hB : B ≤ 1) : S.opTensor A B ≤ S.L A

If 0 ≤ A and B ≤ 1, then A ⊗ B ≤ A ⊗ 1 = L A.

theorem MIPRE.LIDT.Co.SymModel.opTensor_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A B : 𝔓} (hA0 : 0 ≤ A) (hA : A ≤ 1) (hB : B ≤ 1) : S.opTensor A B ≤ 1

A product placement of two effects is an effect: A ⊗ B ≤ L A ≤ 1.