The summed semidefinite form in a commutant with a vector trace

The self-improvement step of the low-individual-degree soundness proof (JNVWY, Lemma 9.2) solves a semidefinite program in the local algebra: it needs a measurement T and an operator Z with Aᵢ ≤ Z for every i and the complementary slackness Tᵢ Z = Tᵢ Aᵢ. The finite-dimensional proof gets them from strong duality. In a finite pair (MIPRE/Foundations/FinitePair.lean) there is no dimension, but there is a faithful trace given by finitely many vectors, and that is enough: a maximizer of T ↦ ∑ᵢ Re τ(Tᵢ Aᵢ) over the measurements of the algebra satisfies a first-order condition, and the first-order condition gives Z := ∑ᵢ Tᵢ Aᵢ self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ. This is reports/c6b-paper-proofs.md, §5 (Theorem 10 with Lemmas 1–9 and 7′, and Corollary 11), item M9 of planning/c6b-plan.md.

Setting (S). t is any set of operators on a Hilbert space H, and the algebra is its commutant StarSubalgebra.centralizer ℂ t (the operators commuting with t and t⋆). The vectors ξ : ι → H, finitely many, give the functional τ(x) = ∑ₖ ⟪ξₖ, x ξₖ⟫ on all of B(H) (tr), which is assumed tracial and faithful on the commutant (IsFaithfulTrace). No normalization is needed. The algebras of a finite pair are of this form, opsA the commutant of opsB and conversely, with the pair's VecTrace.

• IsSummedSdp A T Z: the conclusion, over any ordered ⋆-ring, with the fields of the vendored SdpOptimalPairWithSlackness (Corollary 11): T a measurement, Z self-adjoint, Aᵢ ≤ Z and Tᵢ Z = Tᵢ Aᵢ. Its consumers use slackness only through ∑ᵢ Tᵢ Aᵢ = Z (IsSummedSdp.sum_mul_eq). isSummedSdp_coe_iff moves it between a ⋆-subalgebra and B(H).
• The core chain (Lemmas 1b–3 and 5–9): the trace facts (re_tr_star, re_tr_star_mul_self, eq_zero_of_re_tr_star_mul_self_nonpos), positivity of the pairing of two positive elements (re_tr_mul_nonneg, mul_eq_zero_of_re_tr_mul_nonpos), the perturbed measurement perturb and its exact expansion (isMeasIn_perturb, obj_perturb), the first order condition of a maximizer (firstOrder_of_isMaxOn), and from it the domination (le_of_firstOrder) and slackness (mul_eq_of_le).
• isSummedSdp_of_firstOrder and isSummedSdp_of_isMaxOn: Theorem 10, given a maximizer; and isSummedSdp_of_le, the converse of Corollary 11: self-adjointness and domination give slackness.

That a maximizer exists (Lemma 4) is weak-operator compactness of the unit ball, which the repository has only in the vendored orthonormalization tree, so it and the assembled theorem are MIPRE/Background/Orthonormalization/SdpMaximizer.lean.

The conclusion

structure MIPRE.SummedSdp.IsSummedSdp {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {G : Type u_2} [Fintype G] (A T : G → R) (Z : R) : Prop

The summed semidefinite form (reports/c6b-paper-proofs.md, §5, Corollary 11): T is a measurement (Tᵢ ≥ 0, ∑ᵢ Tᵢ = 1), Z is self-adjoint and dominates every Aᵢ, and Tᵢ Z = Tᵢ Aᵢ for every i. The last three fields are those of the vendored SdpOptimalPairWithSlackness (primalTotalOperator, dualFeasible, complementarySlackness).

• nonneg (i : G) : 0 ≤ T i

  Each outcome is positive.

• total : ∑ i : G, T i = 1

  The outcomes sum to one.

• isSelfAdjoint : IsSelfAdjoint Z

  The dual operator is self-adjoint.

• dualFeasible (i : G) : A i ≤ Z

  Dual feasibility: the dual operator dominates every Aᵢ.

• complementarySlackness (i : G) : T i * Z = T i * A i

  Complementary slackness: Tᵢ Z = Tᵢ Aᵢ.

theorem MIPRE.SummedSdp.IsSummedSdp.sum_mul_eq {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {G : Type u_2} [Fintype G] {A T : G → R} {Z : R} (h : IsSummedSdp A T Z) : ∑ i : G, T i * A i = Z

The composite rewrite the consumers use: in the summed form, ∑ᵢ Tᵢ Aᵢ = Z.

theorem MIPRE.SummedSdp.isSummedSdp_map_iff {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {G : Type u_2} [Fintype G] {S : Type u_3} [Ring S] [StarRing S] [PartialOrder S] (f : R →+* S) (hf : Function.Injective ⇑f) (hstar : ∀ (x : R), f (star x) = star (f x)) (hle : ∀ (x y : R), f x ≤ f y ↔ x ≤ y) {A T : G → R} {Z : R} : IsSummedSdp (fun (i : G) => f (A i)) (fun (i : G) => f (T i)) (f Z) ↔ IsSummedSdp A T Z

The summed form under an order embedding: a ⋆-ring homomorphism that preserves and reflects the order carries the summed form both ways.

theorem MIPRE.SummedSdp.isSummedSdp_coe_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] {S : StarSubalgebra ℂ (H →L[ℂ] H)} {A T : G → ↥S} {Z : ↥S} : IsSummedSdp (fun (i : G) => ↑(A i)) (fun (i : G) => ↑(T i)) ↑Z ↔ IsSummedSdp A T Z

The summed form in a ⋆-subalgebra of B(H) is the summed form of the operators: the subalgebra carries the order of B(H).

The vector functional (Lemma 2)

noncomputable def MIPRE.SummedSdp.tr {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) : (H →L[ℂ] H) →ₗ[ℂ] ℂ

The vector functional τ(x) = ∑ₖ ⟪ξₖ, x ξₖ⟫ of finitely many vectors, on all of B(H).

Equations

• MIPRE.SummedSdp.tr ξ = { toFun := fun (x : H →L[ℂ] H) => ∑ k : ι, inner ℂ (ξ k) (x (ξ k)), map_add' := ⋯, map_smul' := ⋯ }

theorem MIPRE.SummedSdp.tr_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (x : H →L[ℂ] H) : (tr ξ) x = ∑ k : ι, inner ℂ (ξ k) (x (ξ k))

theorem MIPRE.SummedSdp.tr_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (x : H →L[ℂ] H) : (tr ξ) (star x) = (starRingEnd ℂ) ((tr ξ) x)

τ(x⋆) = conj τ(x).

theorem MIPRE.SummedSdp.re_tr_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (x : H →L[ℂ] H) : ((tr ξ) (star x)).re = ((tr ξ) x).re

Re τ(x⋆) = Re τ(x) (Lemma 2).

theorem MIPRE.SummedSdp.re_tr_star_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (x : H →L[ℂ] H) : ((tr ξ) (star x * x)).re = ∑ k : ι, ‖x (ξ k)‖ ^ 2

Re τ(x⋆ x) = ∑ₖ ‖x ξₖ‖² (Lemma 2).

theorem MIPRE.SummedSdp.re_tr_star_mul_self_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (x : H →L[ℂ] H) : 0 ≤ ((tr ξ) (star x * x)).re

Re τ(x⋆ x) ≥ 0 (Lemma 2).

structure MIPRE.SummedSdp.IsFaithfulTrace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (t : Set (H →L[ℂ] H)) (ξ : ι → H) : Prop

Setting (S): the vectors ξ give a tracial functional on the commutant of t, and they separate it, so that the functional is faithful there.

• trace_mul_comm (x : H →L[ℂ] H) : x ∈ StarSubalgebra.centralizer ℂ t → ∀ y ∈ StarSubalgebra.centralizer ℂ t, (tr ξ) (x * y) = (tr ξ) (y * x)

  (Tr): τ(xy) = τ(yx) on the commutant.

• separating (x : H →L[ℂ] H) : x ∈ StarSubalgebra.centralizer ℂ t → (∀ (k : ι), x (ξ k) = 0) → x = 0

  (F): an element of the commutant vanishing at every ξₖ vanishes.

theorem MIPRE.SummedSdp.IsFaithfulTrace.eq_zero_of_re_tr_star_mul_self_nonpos {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {t : Set (H →L[ℂ] H)} {ξ : ι → H} (hS : IsFaithfulTrace t ξ) {x : H →L[ℂ] H} (hx : x ∈ StarSubalgebra.centralizer ℂ t) (h : ((tr ξ) (star x * x)).re ≤ 0) : x = 0

Faithfulness (Lemma 2): an element x of the commutant with Re τ(x⋆ x) ≤ 0 is zero.

The commutant is closed under the functional calculus (Lemma 1b)

theorem MIPRE.SummedSdp.cfcₙ_mem_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {t : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} (hx : x ∈ StarSubalgebra.centralizer ℂ t) (f : ℝ → ℝ) : cfcₙ f x ∈ StarSubalgebra.centralizer ℂ t

The commutant is closed under the real functional calculus (Lemma 1b).

theorem MIPRE.SummedSdp.sqrt_mem_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {t : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} (hx : x ∈ StarSubalgebra.centralizer ℂ t) : CFC.sqrt x ∈ StarSubalgebra.centralizer ℂ t

The commutant contains the square roots of its elements (Lemma 1b).

theorem MIPRE.SummedSdp.negPart_mem_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {t : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} (hx : x ∈ StarSubalgebra.centralizer ℂ t) : x⁻ ∈ StarSubalgebra.centralizer ℂ t

The commutant contains the negative parts of its elements (Lemma 1b).

theorem MIPRE.SummedSdp.real_smul_mem_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {t : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} (hx : x ∈ StarSubalgebra.centralizer ℂ t) (r : ℝ) : r • x ∈ StarSubalgebra.centralizer ℂ t

A real multiple of an element of the commutant is in the commutant.

Positivity of the pairing (Lemma 3)

theorem MIPRE.SummedSdp.re_tr_mul_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {t : Set (H →L[ℂ] H)} {ξ : ι → H} (hS : IsFaithfulTrace t ξ) {T D : H →L[ℂ] H} (hT : T ∈ StarSubalgebra.centralizer ℂ t) (hD : D ∈ StarSubalgebra.centralizer ℂ t) (hT0 : 0 ≤ T) (hD0 : 0 ≤ D) : 0 ≤ ((tr ξ) (T * D)).re

The pairing of two positive elements is positive (Lemma 3): Re τ(T D) ≥ 0.

theorem MIPRE.SummedSdp.mul_eq_zero_of_re_tr_mul_nonpos {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {t : Set (H →L[ℂ] H)} {ξ : ι → H} (hS : IsFaithfulTrace t ξ) {T D : H →L[ℂ] H} (hT : T ∈ StarSubalgebra.centralizer ℂ t) (hD : D ∈ StarSubalgebra.centralizer ℂ t) (hT0 : 0 ≤ T) (hD0 : 0 ≤ D) (h : ((tr ξ) (T * D)).re ≤ 0) : D * T = 0

The equality case of Lemma 3: if two positive elements of the commutant have Re τ(T D) ≤ 0, then D T = 0.

Measurements, the objective, and the perturbation (Lemmas 5 and 6)

structure MIPRE.SummedSdp.IsMeasIn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] (t : Set (H →L[ℂ] H)) (T : G → H →L[ℂ] H) : Prop

A measurement in the commutant: positive elements of the commutant summing to one.

• mem (i : G) : T i ∈ StarSubalgebra.centralizer ℂ t

  Each outcome is in the commutant.

• nonneg (i : G) : 0 ≤ T i

  Each outcome is positive.

• sum_eq_one : ∑ i : G, T i = 1

  The outcomes sum to one.

theorem MIPRE.SummedSdp.IsMeasIn.norm_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} {T : G → H →L[ℂ] H} (hT : IsMeasIn t T) (i : G) : ‖T i‖ ≤ 1

The outcomes of a measurement are contractions: 0 ≤ Tᵢ ≤ ∑ⱼ Tⱼ = 1.

noncomputable def MIPRE.SummedSdp.obj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] {G : Type u_3} [Fintype G] (ξ : ι → H) (A T : G → H →L[ℂ] H) : ℝ

The objective f(T) = ∑ᵢ Re τ(Tᵢ Aᵢ).

Equations

• MIPRE.SummedSdp.obj ξ A T = ∑ i : G, ((MIPRE.SummedSdp.tr ξ) (T i * A i)).re

def MIPRE.SummedSdp.FirstOrder {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) (A T : G → H →L[ℂ] H) : Prop

The first-order condition FO(T, A): Re τ(P Aₕ) ≤ Re τ(P Z) for every h and every P of the commutant with 0 ≤ P ≤ 1, where Z = ∑ᵢ Tᵢ Aᵢ.

Equations

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

noncomputable def MIPRE.SummedSdp.perturb {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {G : Type u_3} [DecidableEq G] (T : G → H →L[ℂ] H) (h : G) (K : H →L[ℂ] H) : G → H →L[ℂ] H

The perturbed measurement of Lemma 5: T'ᵢ = K Tᵢ K + δᵢₕ (1 - K²).

Equations

• MIPRE.SummedSdp.perturb T h K i = K * T i * K + if i = h then 1 - K * K else 0

theorem MIPRE.SummedSdp.isMeasIn_perturb {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} [DecidableEq G] {T : G → H →L[ℂ] H} (hT : IsMeasIn t T) (h : G) {P : H →L[ℂ] H} (hP : P ∈ StarSubalgebra.centralizer ℂ t) (hP0 : 0 ≤ P) (hP1 : P ≤ 1) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : IsMeasIn t (perturb T h (1 - ε • P))

The perturbed measurement is a measurement (Lemma 5): for P in the commutant with 0 ≤ P ≤ 1 and 0 ≤ ε ≤ 1, with K = 1 - εP.

theorem MIPRE.SummedSdp.re_tr_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] (ξ : ι → H) (r : ℝ) (x : H →L[ℂ] H) : ((tr ξ) (r • x)).re = r * ((tr ξ) x).re

Re τ(r • x) = r Re τ(x) for real r.

theorem MIPRE.SummedSdp.re_tr_swap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {t : Set (H →L[ℂ] H)} {ξ : ι → H} (hS : IsFaithfulTrace t ξ) {T P A : H →L[ℂ] H} (hT : T ∈ StarSubalgebra.centralizer ℂ t) (hP : P ∈ StarSubalgebra.centralizer ℂ t) (hA : A ∈ StarSubalgebra.centralizer ℂ t) (hTsa : IsSelfAdjoint T) (hPsa : IsSelfAdjoint P) (hAsa : IsSelfAdjoint A) : ((tr ξ) (T * P * A)).re = ((tr ξ) (P * T * A)).re

The swap of Lemma 6: for self-adjoint T, P, A of the commutant, Re τ(T P A) = Re τ(P T A).

theorem MIPRE.SummedSdp.obj_perturb {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} [DecidableEq G] (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (h : G) {P : H →L[ℂ] H} (hP : P ∈ StarSubalgebra.centralizer ℂ t) (hPsa : IsSelfAdjoint P) (ε : ℝ) : obj ξ A (perturb T h (1 - ε • P)) = obj ξ A T + 2 * ε * (((tr ξ) (P * A h)).re - ((tr ξ) (P * ∑ i : G, T i * A i)).re) + ε ^ 2 * (∑ i : G, ((tr ξ) (P * T i * P * A i)).re - ((tr ξ) (P * P * A h)).re)

The exact expansion (Lemma 6): with K = 1 - εP and Z = ∑ᵢ Tᵢ Aᵢ, f(T') = f(T) + 2ε (Re τ(P Aₕ) - Re τ(P Z)) + ε² c with c = ∑ᵢ Re τ(P Tᵢ P Aᵢ) - Re τ(P² Aₕ).

The first-order condition (Lemmas 7 and 7′)

theorem MIPRE.SummedSdp.nonpos_of_quadratic {a c : ℝ} (h : ∀ (ε : ℝ), 0 ≤ ε → ε ≤ 1 → 2 * ε * a + ε ^ 2 * c ≤ 0) : a ≤ 0

A quadratic first-order lemma (Lemma 7): if 2εa + ε²c ≤ 0 for every ε ∈ [0, 1], then a ≤ 0.

theorem MIPRE.SummedSdp.firstOrder_of_isMaxOn {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (hmax : IsMaxOn (obj ξ A) {T : G → H →L[ℂ] H | IsMeasIn t T} T) : FirstOrder t ξ A T

A maximizer satisfies the first-order condition (Lemma 7′).

Domination and slackness (Lemmas 8 and 9)

theorem MIPRE.SummedSdp.re_tr_mul_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {t : Set (H →L[ℂ] H)} {ξ : ι → H} (hS : IsFaithfulTrace t ξ) {P Z : H →L[ℂ] H} (hP : P ∈ StarSubalgebra.centralizer ℂ t) (hZ : Z ∈ StarSubalgebra.centralizer ℂ t) (hPsa : IsSelfAdjoint P) : ((tr ξ) (P * star Z)).re = ((tr ξ) (P * Z)).re

The pairing with Z⋆ (Lemma 8, step 1): for a self-adjoint P and Z in the commutant, Re τ(P Z⋆) = Re τ(P Z).

theorem MIPRE.SummedSdp.sum_mul_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} {T A : G → H →L[ℂ] H} (hT : ∀ (i : G), T i ∈ StarSubalgebra.centralizer ℂ t) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) : ∑ i : G, T i * A i ∈ StarSubalgebra.centralizer ℂ t

Z = ∑ᵢ Tᵢ Aᵢ is in the commutant.

theorem MIPRE.SummedSdp.le_of_firstOrder {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (hFO : FirstOrder t ξ A T) (h : G) : A h ≤ 2⁻¹ • (∑ i : G, T i * A i + star (∑ i : G, T i * A i))

Domination by the real part (Lemma 8): under the first-order condition, W = (Z + Z⋆)/2 dominates every Aₕ.

theorem MIPRE.SummedSdp.mul_eq_of_le {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) {W : H →L[ℂ] H} (hW : W ∈ StarSubalgebra.centralizer ℂ t) (hle : ∀ (i : G), A i ≤ W) (htr : ((tr ξ) W).re ≤ ((tr ξ) (∑ i : G, T i * A i)).re) (i : G) : W * T i = A i * T i

Slackness (Lemma 9, steps 1–3): if a self-adjoint W of the commutant dominates every Aᵢ and Re τ(W) ≤ Re τ(Z) with Z = ∑ᵢ Tᵢ Aᵢ, then W Tᵢ = Aᵢ Tᵢ for every i.

theorem MIPRE.SummedSdp.eq_star_of_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {G : Type u_3} [Fintype G] {t : Set (H →L[ℂ] H)} {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) {W : H →L[ℂ] H} (hWT : ∀ (i : G), W * T i = A i * T i) : W = star (∑ i : G, T i * A i)

W = Z⋆ (Lemma 9, step 4): if W Tᵢ = Aᵢ Tᵢ for every i, with the Aᵢ self-adjoint and T a measurement, then W = (∑ᵢ Tᵢ Aᵢ)⋆.

Theorem 10 and Corollary 11

theorem MIPRE.SummedSdp.isSummedSdp_of_firstOrder {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (hFO : FirstOrder t ξ A T) : IsSummedSdp A T (∑ i : G, T i * A i)

The summed semidefinite form from the first-order condition (reports/c6b-paper-proofs.md, §5, Theorem 10 via Lemmas 8 and 9): if a measurement T of the commutant satisfies FO(T, A) for self-adjoint Aᵢ of the commutant, then Z = ∑ᵢ Tᵢ Aᵢ is self-adjoint, dominates every Aᵢ, and Tᵢ Z = Tᵢ Aᵢ.

theorem MIPRE.SummedSdp.isSummedSdp_of_isMaxOn {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (hmax : IsMaxOn (obj ξ A) {T : G → H →L[ℂ] H | IsMeasIn t T} T) : IsSummedSdp A T (∑ i : G, T i * A i)

Theorem 10, given a maximizer (reports/c6b-paper-proofs.md, §5): a maximizer of T ↦ ∑ᵢ Re τ(Tᵢ Aᵢ) over the measurements of the commutant gives the summed semidefinite form, with Z = ∑ᵢ Tᵢ Aᵢ.

theorem MIPRE.SummedSdp.isSummedSdp_of_le {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} (hS : IsFaithfulTrace t ξ) {T A : G → H →L[ℂ] H} (hT : IsMeasIn t T) (hA : ∀ (i : G), A i ∈ StarSubalgebra.centralizer ℂ t) (hAsa : ∀ (i : G), IsSelfAdjoint (A i)) (hZsa : IsSelfAdjoint (∑ i : G, T i * A i)) (hle : ∀ (i : G), A i ≤ ∑ i : G, T i * A i) : IsSummedSdp A T (∑ i : G, T i * A i)

The converse of Corollary 11: if Z = ∑ᵢ Tᵢ Aᵢ is self-adjoint and dominates every Aᵢ, for a measurement T of the commutant, then complementary slackness holds.