The summed semidefinite form in the doubled model

Corollary 12 and Lemma 13 of reports/c6b-paper-proofs.md, §5.5–5.6 (item M9 of planning/c6b-plan.md). Theorem 10 (MIPRE.Orthonormalization.exists_isSummedSdp_finitePairA, _finitePairB) solves the summed semidefinite program IsSummedSdp A T Z (a measurement T, a self-adjoint Z ≥ Aᵢ, Tᵢ Z = Tᵢ Aᵢ) in each commutant of a finite pair M. This file solves it in the doubled model's local algebra and carries the solution to the placements and to the players' abstract algebras.

• Componentwise (isSummedSdp_prod_iff): in a product of ordered ⋆-rings, with the componentwise order, the summed form holds exactly when it holds in each factor.
• Corollary 12 (exists_isSummedSdp_loc): for self-adjoint Aᵢ of the doubled local algebra Loc M = LocA M × LocB M, the solutions of Theorem 10 in LocA M and in LocB M, paired, solve the program in Loc M, with Z = ∑ᵢ Tᵢ Aᵢ; and so do their images under both placements of the doubled model (isSummedSdp_L_iff, isSummedSdp_R_iff, exists_isSummedSdp_model). Neither the property (S) of the doubled algebra nor a doubled trace is used.
• Lemma 13 (isSummedSdp_equivA_iff, isSummedSdp_equiv_iff): the summed form pulls back along the ⋆-isomorphisms IsFinitePair.equivA : 𝒜 ≃⋆ₐ LocA M and Doubling.equiv : 𝒜 × ℬ ≃⋆ₐ Loc M of a finite pair with star-ordered algebras, and pushes forward. The order agreement it rests on is IsFinitePair.nonneg_iff_A (MIPRE/Foundations/FinitePairOrder.lean), not re-proved here; a measurement pulls back by POVMIn.mapHom hM.equivA.symm. So Theorem 10 holds in 𝒜 itself (exists_isSummedSdp_A, exists_isSummedSdp_B), and Corollary 12 in the report's local algebra 𝒩 = 𝒜 × ℬ (exists_isSummedSdp_prod), with the images under the placements of the translation.

The order transport is one lemma (isSummedSdp_map_iff_of_nonneg_iff): a ⋆-ring homomorphism between star-ordered rings that reflects nonnegativity is an order embedding, injective, and carries the summed form both ways.

Transport of the summed form

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_prod_iff {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [Ring S] [StarRing S] [PartialOrder S] {G : Type u_3} [Fintype G] {A T : G → R × S} {Z : R × S} : SummedSdp.IsSummedSdp A T Z ↔ SummedSdp.IsSummedSdp (fun (i : G) => (A i).1) (fun (i : G) => (T i).1) Z.1 ∧ SummedSdp.IsSummedSdp (fun (i : G) => (A i).2) (fun (i : G) => (T i).2) Z.2

The summed form in a product is the summed form in each factor: the operations, the star and the order of R × S are componentwise.

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_map_iff_of_nonneg_iff {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [Ring S] [StarRing S] [PartialOrder S] {G : Type u_3} [Fintype G] [StarOrderedRing R] [StarOrderedRing S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] [StarHomClass F R S] (f : F) (hf : ∀ (x : R), 0 ≤ f x ↔ 0 ≤ x) {A T : G → R} {Z : R} : SummedSdp.IsSummedSdp (fun (i : G) => f (A i)) (fun (i : G) => f (T i)) (f Z) ↔ SummedSdp.IsSummedSdp A T Z

The summed form along a homomorphism that reflects nonnegativity: a ⋆-ring homomorphism f between star-ordered rings with 0 ≤ f x ↔ 0 ≤ x preserves and reflects the order, is injective, and so carries the summed form both ways.

Corollary 12: the doubled model's local algebra

theorem MIPRE.LIDT.Co.Doubling.exists_isSummedSdp_loc {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [Nonempty G] (A : G → Loc M) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → Loc M), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Corollary 12 (reports/c6b-paper-proofs.md, §5.5): in the doubled local algebra Loc M = LocA M × LocB M of a finite pair, for finitely many self-adjoint Aᵢ there is a measurement T with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ. It is solved componentwise, by Theorem 10 in LocA M and in LocB M.

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_L_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {G : Type u_4} [Fintype G] {A T : G → Loc M} {Z : Loc M} : SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).L (A i)) (fun (i : G) => (model hM hψ).L (T i)) ((model hM hψ).L Z) ↔ SummedSdp.IsSummedSdp A T Z

The summed form under the first placement of the doubled model: L preserves and reflects the order (L_nonneg_iff), so it carries the summed form both ways.

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_R_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {G : Type u_4} [Fintype G] {A T : G → Loc M} {Z : Loc M} : SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).R (A i)) (fun (i : G) => (model hM hψ).R (T i)) ((model hM hψ).R Z) ↔ SummedSdp.IsSummedSdp A T Z

The summed form under the second placement of the doubled model: R preserves and reflects the order (R_nonneg_iff), so it carries the summed form both ways.

theorem MIPRE.LIDT.Co.Doubling.exists_isSummedSdp_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {G : Type u_4} [Fintype G] [Nonempty G] (A : G → Loc M) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → Loc M), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i) ∧ SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).L (A i)) (fun (i : G) => (model hM hψ).L (T i)) ((model hM hψ).L (∑ i : G, T i * A i)) ∧ SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).R (A i)) (fun (i : G) => (model hM hψ).R (T i)) ((model hM hψ).R (∑ i : G, T i * A i))

Corollary 12 with the placements (reports/c6b-paper-proofs.md, §5.5): for finitely many self-adjoint Aᵢ of the doubled local algebra there is a measurement T that, with Z = ∑ᵢ Tᵢ Aᵢ, solves the summed form in Loc M and under both placements L and R.

Lemma 13: pull-back to the players' algebras

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_equivA_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {A T : G → 𝒜} {Z : 𝒜} : SummedSdp.IsSummedSdp (fun (i : G) => hM.equivA (A i)) (fun (i : G) => hM.equivA (T i)) (hM.equivA Z) ↔ SummedSdp.IsSummedSdp A T Z

Lemma 13, first player (reports/c6b-paper-proofs.md, §5.6): the summed form pulls back along IsFinitePair.equivA : 𝒜 ≃⋆ₐ LocA M and pushes forward, by the order agreement IsFinitePair.nonneg_iff_A.

theorem MIPRE.LIDT.Co.Doubling.exists_isSummedSdp_A {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Nonempty G] (A : G → 𝒜) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → 𝒜), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 in the first player's algebra of a finite pair (Theorem 10 in LocA M, pulled back by Lemma 13): for finitely many self-adjoint Aᵢ ∈ 𝒜 there is a measurement T of 𝒜 with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ.

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_equivB_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [PartialOrder ℬ] [StarOrderedRing ℬ] {A T : G → ℬ} {Z : ℬ} : SummedSdp.IsSummedSdp (fun (i : G) => hM.equivB (A i)) (fun (i : G) => hM.equivB (T i)) (hM.equivB Z) ↔ SummedSdp.IsSummedSdp A T Z

Lemma 13, second player: the summed form pulls back along IsFinitePair.equivB : ℬ ≃⋆ₐ LocB M and pushes forward, by IsFinitePair.nonneg_iff_B.

theorem MIPRE.LIDT.Co.Doubling.exists_isSummedSdp_B {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [PartialOrder ℬ] [StarOrderedRing ℬ] [Nonempty G] (A : G → ℬ) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → ℬ), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 in the second player's algebra of a finite pair (Theorem 10 in LocB M, pulled back by Lemma 13).

theorem MIPRE.LIDT.Co.Doubling.isSummedSdp_equiv_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {G : Type u_4} [Fintype G] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {A T : G → 𝒜 × ℬ} {Z : 𝒜 × ℬ} : SummedSdp.IsSummedSdp (fun (i : G) => (equiv hM) (A i)) (fun (i : G) => (equiv hM) (T i)) ((equiv hM) Z) ↔ SummedSdp.IsSummedSdp A T Z

Lemma 13 for the report's local algebra 𝒩 = 𝒜 × ℬ: the summed form pulls back along the translation Doubling.equiv : 𝒜 × ℬ ≃⋆ₐ Loc M and pushes forward (equiv_nonneg_iff).

theorem MIPRE.LIDT.Co.Doubling.exists_isSummedSdp_prod {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {G : Type u_4} [Fintype G] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [Nonempty G] (A : G → 𝒜 × ℬ) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → 𝒜 × ℬ), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i) ∧ SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).L ((equiv hM) (A i))) (fun (i : G) => (model hM hψ).L ((equiv hM) (T i))) ((model hM hψ).L ((equiv hM) (∑ i : G, T i * A i))) ∧ SummedSdp.IsSummedSdp (fun (i : G) => (model hM hψ).R ((equiv hM) (A i))) (fun (i : G) => (model hM hψ).R ((equiv hM) (T i))) ((model hM hψ).R ((equiv hM) (∑ i : G, T i * A i)))

Corollary 12 in the report's local algebra 𝒩 = 𝒜 × ℬ (reports/c6b-paper-proofs.md, §5.5–5.6): for finitely many self-adjoint Aᵢ ∈ 𝒜 × ℬ there is a measurement T of 𝒜 × ℬ that, with Z = ∑ᵢ Tᵢ Aᵢ, solves the summed form in 𝒜 × ℬ, and whose translation solves it under both placements of the doubled model.