Section 9 -- Canonical SDP separation argument

This module contains the closed-image-cone separation argument and the resulting zero-duality-gap theorem for the canonical finite-dimensional matrix SDP.

References

• references/ldt-paper/self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalConeMap (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model) →L[ℝ] MakingMeasurementsProjective.MatrixOperator model.space × ℝ

The map sending a primal matrix to its constraint image and objective value.

Equations

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalConeMap_apply (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : (matrixSdpCanonicalPrimalConeMap params model) X = (matrixSdpCanonicalConstraintOperator params model X, (matrixSdpCanonicalObjectiveOperator params model * X).trace.re)

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ProperCone ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)

The closed image cone of positive semidefinite canonical primal matrices under the constraint-objective map.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone_mem_of_nonnegative (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : 0 ≤ X) : (matrixSdpCanonicalConstraintOperator params model X, (matrixSdpCanonicalObjectiveOperator params model * X).trace.re) ∈ matrixSdpCanonicalPrimalImageCone params model

An actual positive semidefinite canonical primal matrix maps into the closed canonical primal image cone.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone_mem_of_feasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : (1, (matrixSdpCanonicalObjectiveOperator params model * X).trace.re) ∈ matrixSdpCanonicalPrimalImageCone params model

A feasible canonical primal matrix maps to the image-cone point with constraint component equal to the identity.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone_identity_mem_iff_exists_feasible_objective (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (t : ℝ) : (1, t) ∈ matrixSdpCanonicalPrimalImageCone params model ↔ ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model X ∧ (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = t

On the identity constraint fiber, the closed primal image cone contains exactly the objective values of feasible canonical primal matrices.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone_notMem_identity_of_primalMax_lt (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) {Xmax : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)} {t : ℝ} (_hXmax : MatrixSdpCanonicalPrimalFeasible params model Xmax) (hmax : ∀ (Y : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model Y → (matrixSdpCanonicalObjectiveOperator params model * Y).trace.re ≤ (matrixSdpCanonicalObjectiveOperator params model * Xmax).trace.re) (hlt : (matrixSdpCanonicalObjectiveOperator params model * Xmax).trace.re < t) : (1, t) ∉ matrixSdpCanonicalPrimalImageCone params model

If Xmax maximizes the canonical primal objective and t is strictly above its value, then the identity-fiber point with objective coordinate t is not in the closed primal image cone.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalImageCone_separation_of_notMem (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) {y : MakingMeasurementsProjective.MatrixOperator model.space × ℝ} (hy : y ∉ matrixSdpCanonicalPrimalImageCone params model) : ∃ (f : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)), (∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, 0 ≤ f z) ∧ f y < 0

A point outside the canonical primal image cone has a continuous real-linear separator.

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSeparatorObjectiveCoefficient {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) : ℝ

Section 9 notation for the objective-coordinate coefficient of a separator.

The calculation is supplied by the shared conic-separation layer in MIPStarRE.Quantum.FiniteConicDuality; this abbreviation preserves the matrix-SDP statement surface used by the source-labelled Section 9 lemmas.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSeparatorObjectiveCoefficient φ = MIPStarRE.Quantum.conicSeparatorObjectiveCoefficient φ

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorDualMatrix {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) : MakingMeasurementsProjective.MatrixOperator model.space

The Hermitian matrix representing the normalized separator functional under the real trace pairing.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorDualMatrix φ = MIPStarRE.Quantum.hermitianTracePairingMatrixOfRealCLM (MIPStarRE.Quantum.conicNormalizedSeparatorFunctional φ)

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorDualMatrix_isHermitian {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) : Matrix.IsHermitian (matrixSdpCanonicalNormalizedSeparatorDualMatrix φ)

The matrix representing the normalized separator is Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorFunctional_eq_trace_dualMatrix {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) {Y : MakingMeasurementsProjective.MatrixOperator model.space} (hY : Matrix.IsHermitian Y) : (Quantum.conicNormalizedSeparatorFunctional φ) Y = (matrixSdpCanonicalNormalizedSeparatorDualMatrix φ * Y).trace.re

On Hermitian inputs, the normalized separator functional is the real trace pairing against its Hermitian representing matrix.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalTracePairingDualMatrix_dualFeasible_of_conicFunctionalDualFeasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (ψ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space)) (hψ : ∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, z.2 ≤ ψ z.1) (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model (Quantum.hermitianTracePairingMatrixOfRealCLM ψ) g

A feasible functional dual bound on the canonical primal image cone gives a paper-form dual feasible matrix through the Hermitian trace-pairing representation.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalFunctionalDualObjective_min_of_matrixDualMin (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hZmin : ∀ (W : MakingMeasurementsProjective.MatrixOperator model.space), (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model W g) → matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model W) (ψ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space)) : (∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, z.2 ≤ ψ z.1) → matrixSdpDualObjective model Z ≤ ψ 1

A paper-form dual minimizer is also minimal among feasible functional dual bounds on the canonical primal image cone.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjective_le_normalizedSeparatorDualMatrix_on_nonnegative (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) (hφ : ∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, 0 ≤ φ z) (hcoeff : matrixSdpCanonicalSeparatorObjectiveCoefficient φ < 0) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : 0 ≤ X) : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re ≤ (matrixSdpCanonicalDualOperator params model (matrixSdpCanonicalNormalizedSeparatorDualMatrix φ) * X).trace.re

The normalized separator matrix dominates the canonical objective on every positive canonical primal cone point.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorDualMatrix_dualFeasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) (hφ : ∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, 0 ≤ φ z) (hcoeff : matrixSdpCanonicalSeparatorObjectiveCoefficient φ < 0) (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model (matrixSdpCanonicalNormalizedSeparatorDualMatrix φ) g

The normalized separator matrix is paper-form dual feasible.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNormalizedSeparatorDualMatrix_dualObjective_lt_of_sep {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) {t : ℝ} (hsep : φ (1, t) < 0) (hcoeff : matrixSdpCanonicalSeparatorObjectiveCoefficient φ < 0) : matrixSdpDualObjective model (matrixSdpCanonicalNormalizedSeparatorDualMatrix φ) < t

The normalized separator matrix has dual objective below the separated objective coordinate.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSeparator_exists_dualFeasible_lt_of_feasible_lt (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (φ : StrongDual ℝ (MakingMeasurementsProjective.MatrixOperator model.space × ℝ)) {t : ℝ} (hφ : ∀ z ∈ matrixSdpCanonicalPrimalImageCone params model, 0 ≤ φ z) (hsep : φ (1, t) < 0) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (hXlt : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re < t) : ∃ (W : MakingMeasurementsProjective.MatrixOperator model.space), (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model W g) ∧ matrixSdpDualObjective model W < t

A separating functional above a feasible primal value produces a better dual-feasible point.

Paper origin: references/ldt-paper/self_improvement.tex lines 82--190 (\label{lem:sdp}). This is the normalized-separator step in the proof of strong duality for the canonical SDP: separating the point (I,t) from the closed primal image cone gives, through the real trace-pairing representative of the normalized constraint functional, a dual-feasible matrix whose dual objective is strictly below t.

This lemma is a Lean-only organization of the separation proof. It does not change the paper-facing statement of lem:sdp.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalObjective_exists_isMaxOn (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model X ∧ ∀ (Y : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model Y → (matrixSdpCanonicalObjectiveOperator params model * Y).trace.re ≤ (matrixSdpCanonicalObjectiveOperator params model * X).trace.re

The canonical primal objective attains a maximum on the feasible set.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalDualOptima_exist (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (Z : MakingMeasurementsProjective.MatrixOperator model.space), MatrixSdpCanonicalPrimalFeasible params model X ∧ (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ (∀ (Y : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model Y → (matrixSdpCanonicalObjectiveOperator params model * Y).trace.re ≤ (matrixSdpCanonicalObjectiveOperator params model * X).trace.re) ∧ (∀ (W : MakingMeasurementsProjective.MatrixOperator model.space), (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model W g) → matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model W) ∧ (matrixSdpCanonicalObjectiveOperator params model * X).trace.re ≤ matrixSdpDualObjective model Z

The canonical primal maximizer and dual minimizer exist, and their attained values satisfy weak duality. This packages the attained optima but is not the zero-gap strong-duality theorem.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalStrongDuality (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (Z : MakingMeasurementsProjective.MatrixOperator model.space), MatrixSdpCanonicalPrimalFeasible params model X ∧ (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = matrixSdpDualObjective model Z

The canonical matrix SDP has a primal-dual optimal pair with zero duality gap.

This is the finite-dimensional strong-duality conclusion used in the paper's Section 9 SDP argument. The proof combines compact attainment, separation of the closed primal image cone, and the trace-pairing representation of the normalized separator; it does not add an auxiliary dominance hypothesis on the dual matrix.