The summed semidefinite form: a maximizer, and the theorem

MIPRE/Foundations/SummedSdp.lean proves that a maximizer of T ↦ ∑ᵢ Re τ(Tᵢ Aᵢ) over the measurements of the commutant of a set t of operators, with τ a faithful tracial vector functional there, gives the summed semidefinite form: Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ. This file supplies the maximizer and assembles the theorem (reports/c6b-paper-proofs.md, §5, Lemma 4 and Theorem 10).

• Lemma 4 (exists_isMaxOn_obj): in the product of weak operator topologies, the measurements of the commutant form a closed subset of a product of unit balls, which is compact (the vendored Orthogonalization.MvN.isCompact_setOf_norm_le), and the objective is a finite sum of matrix coefficients, hence continuous. A finite sum of vector functionals is weak-operator continuous, so no σ-weak topology and no predual are needed.
• Theorem 10 (exists_isSummedSdp, and exists_isSummedSdp_centralizer with the measurement and Z in the commutant as a ⋆-subalgebra, carrying the order of B(H)).
• In a finite pair (exists_isSummedSdp_finitePairA, exists_isSummedSdp_finitePairB): the commutant of the second player's operators, StarSubalgebra.centralizer ℂ M.opsB, is the first player's operators, and the pair's VecTrace is faithful and tracial on it; symmetrically for the second player. These are the two components of the doubled model's local algebra centralizer ℂ M.opsB × centralizer ℂ M.opsA (item M2 of planning/c6b-plan.md), in which the join stage solves the program componentwise (Corollary 12) and pulls the solution back to the abstract algebras by order agreement (Lemma 13); neither is done here.

The weak-operator compactness lives in the vendored tree, which only MIPRE/Background/ may name, so this file is here and the core chain is in MIPRE/Foundations.

noncomputable def MIPRE.Orthonormalization.centralizerVN {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (t : Set (H →L[ℂ] H)) : VonNeumannAlgebra H

The commutant of a set of operators as a von Neumann algebra: its M″ = M field is t‴ = t′, so no bicommutant theorem is needed.

Equations

• MIPRE.Orthonormalization.centralizerVN t = { toStarSubalgebra := StarSubalgebra.centralizer ℂ t, centralizer_centralizer' := ⋯ }

theorem MIPRE.Orthonormalization.exists_isMaxOn_obj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {G : Type u_3} [Fintype G] [Nonempty G] (t : Set (H →L[ℂ] H)) (ξ : ι → H) (A : G → H →L[ℂ] H) : ∃ (T : G → H →L[ℂ] H), SummedSdp.IsMeasIn t T ∧ IsMaxOn (SummedSdp.obj ξ A) {T : G → H →L[ℂ] H | SummedSdp.IsMeasIn t T} T

A maximizer exists (reports/c6b-paper-proofs.md, §5, Lemma 4): the objective T ↦ ∑ᵢ Re τ(Tᵢ Aᵢ) attains its maximum on the measurements of the commutant of t, by weak-operator compactness of the unit ball.

theorem MIPRE.Orthonormalization.exists_isSummedSdp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} {ξ : ι → H} [Nonempty G] (hS : SummedSdp.IsFaithfulTrace t ξ) {A : G → H →L[ℂ] H} (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → H →L[ℂ] H), SummedSdp.IsMeasIn t T ∧ SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 (reports/c6b-paper-proofs.md, §5): in the commutant of a set t of operators, with a faithful tracial vector functional, for finitely many self-adjoint Aᵢ of the commutant there is a measurement T of the commutant with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ for every i.

theorem MIPRE.Orthonormalization.exists_isSummedSdp_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} {ξ : ι → H} [Nonempty G] (hS : SummedSdp.IsFaithfulTrace t ξ) (A : G → ↥(StarSubalgebra.centralizer ℂ t)) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → ↥(StarSubalgebra.centralizer ℂ t)), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 in the commutant as a ⋆-subalgebra: for finitely many self-adjoint Aᵢ of the commutant, there is a measurement T of the commutant, in its own order (that of B(H)), with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ for every i.

theorem MIPRE.SummedSdp.IsFaithfulTrace.of_vecTrace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {t s : Set (H →L[ℂ] H)} (τ : VecTrace s) (h : ∀ x ∈ StarSubalgebra.centralizer ℂ t, x ∈ s) : IsFaithfulTrace t τ.g

A vector trace is a faithful trace on a commutant inside its set.

theorem MIPRE.Orthonormalization.exists_isSummedSdp_finitePairA {G : Type u_3} [Fintype G] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hM : M.IsFinitePair) [Nonempty G] (A : G → ↥(StarSubalgebra.centralizer ℂ M.opsB)) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → ↥(StarSubalgebra.centralizer ℂ M.opsB)), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 for the first player of a finite pair: in the commutant of the second player's operators (which are the first player's operators), for finitely many self-adjoint Aᵢ there is a measurement T with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ.

theorem MIPRE.Orthonormalization.exists_isSummedSdp_finitePairB {G : Type u_3} [Fintype G] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hM : M.IsFinitePair) [Nonempty G] (A : G → ↥(StarSubalgebra.centralizer ℂ M.opsA)) (hA : ∀ (i : G), IsSelfAdjoint (A i)) : ∃ (T : G → ↥(StarSubalgebra.centralizer ℂ M.opsA)), SummedSdp.IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10 for the second player of a finite pair: in the commutant of the first player's operators (which are the second player's operators), for finitely many self-adjoint Aᵢ there is a measurement T with Z = ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ.