Section 9 -- Canonical SDP strong-duality preliminaries

This module contains the feasibility, compactness, closedness, and objective-continuity lemmas used in the finite-dimensional strong-duality argument for the canonical matrix SDP.

References

• references/ldt-paper/self_improvement.tex

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_nonempty (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), MatrixSdpCanonicalPrimalFeasible params model X

The canonical primal SDP has a feasible point, supplied by the explicit strict primal submeasurement.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_trace_eq (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : Matrix.trace (matrixSdpCanonicalConstraintOperator params model X) = Matrix.trace X

The canonical equality-constraint operator preserves trace.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalNonnegative_norm_le_constraint_trace_re (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : 0 ≤ X) : ‖X‖ ≤ (Matrix.trace (matrixSdpCanonicalConstraintOperator params model X)).re

A PSD canonical primal variable is norm-controlled by the real trace of its constraint image.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_trace_eq (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : Matrix.trace X = ↑(Fintype.card model.space.carrier)

A feasible canonical primal matrix has trace equal to the base Hilbert-space dimension.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_norm_le (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : ‖X‖ ≤ ↑(Fintype.card model.space.carrier)

Feasible canonical primal matrices have uniformly bounded elementwise norm.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_isBounded (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Bornology.IsBounded {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model) | MatrixSdpCanonicalPrimalFeasible params model X}

The feasible set of the canonical primal SDP is bounded in the elementwise matrix norm.

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

The projection onto one diagonal block of the canonical primal matrix, as a continuous real-linear map.

Equations

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlockCLM_apply (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (b : MatrixSdpCanonicalBlockIndex params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : (matrixSdpCanonicalDiagonalBlockCLM params model b) X = matrixSdpCanonicalDiagonalBlock params model X b

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

The canonical equality-constraint operator as a continuous real-linear map.

Equations

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperatorCLM_apply (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : (matrixSdpCanonicalConstraintOperatorCLM params model) X = matrixSdpCanonicalConstraintOperator params model X

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

The canonical primal objective as a continuous real-linear functional.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.continuous_matrixSdpCanonicalConstraintOperator (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Continuous fun (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) => matrixSdpCanonicalConstraintOperator params model X

The canonical primal equality-constraint operator is continuous.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_isHermitian (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (hB : ∀ (b : MatrixSdpCanonicalBlockIndex params), Matrix.IsHermitian (B b)) : Matrix.IsHermitian (matrixSdpCanonicalBlockDiagonal params model B)

A canonical block-diagonal operator is Hermitian when all diagonal blocks are Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualOperator_isHermitian (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hZ : Matrix.IsHermitian Z) : Matrix.IsHermitian (matrixSdpCanonicalDualOperator params model Z)

The canonical dual block operator is Hermitian when the paper dual matrix is Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjectiveOperator_isHermitian (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Matrix.IsHermitian (matrixSdpCanonicalObjectiveOperator params model)

The canonical objective block operator is Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualOperator_sub_objectiveOperator_isHermitian (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hZ : Matrix.IsHermitian Z) : Matrix.IsHermitian (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model)

The canonical dual slack block operator is Hermitian when the paper dual matrix is Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualOperator_trace_constraint (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (Z : MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalDualOperator params model Z * X).trace.re = (Z * matrixSdpCanonicalConstraintOperator params model X).trace.re

The canonical dual block trace pairing equals the paper dual trace pairing against the canonical constraint image.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_nonneg_of_nonnegative (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)} (hX : 0 ≤ X) : 0 ≤ matrixSdpCanonicalConstraintOperator params model X

The canonical equality-constraint image of a positive canonical primal matrix is positive semidefinite.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_isHermitian_of_nonnegative (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)} (hX : 0 ≤ X) : Matrix.IsHermitian (matrixSdpCanonicalConstraintOperator params model X)

The canonical equality-constraint image of a positive canonical primal matrix is Hermitian.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualConstraint_nonneg_of_trace_pairing_nonneg (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hHerm : Matrix.IsHermitian (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model)) (htrace : ∀ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)), 0 ≤ X → 0 ≤ ((matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) * X).trace.re) (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model Z g

A trace-pairing separator against every positive semidefinite canonical primal matrix can be converted into the paper-form dual feasibility inequalities.

This is a separator-conversion lemma for the later zero-gap argument, not the strong-duality theorem itself.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_isClosed (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : IsClosed {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model) | MatrixSdpCanonicalPrimalFeasible params model X}

The feasible set of the canonical primal SDP is closed.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualFeasible_isClosed (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : IsClosed {Z : MakingMeasurementsProjective.MatrixOperator model.space | ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g}

The paper-form canonical dual feasible set is closed.

theorem MIPStarRE.LDT.SelfImprovement.continuous_matrixSdpDualObjective (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Continuous fun (Z : MakingMeasurementsProjective.MatrixOperator model.space) => matrixSdpDualObjective model Z

The paper-form canonical dual objective is continuous.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualFeasibleSublevel_isClosed (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : IsClosed {Z : MakingMeasurementsProjective.MatrixOperator model.space | (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model (matrixSdpStrictDualWitness model)}

The strict-witness-bounded dual feasible sublevel is closed.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualFeasibleSublevel_isBounded (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Bornology.IsBounded {Z : MakingMeasurementsProjective.MatrixOperator model.space | (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model (matrixSdpStrictDualWitness model)}

The strict-witness-bounded dual feasible sublevel is norm-bounded.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualFeasibleSublevel_isCompact (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : IsCompact {Z : MakingMeasurementsProjective.MatrixOperator model.space | (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model (matrixSdpStrictDualWitness model)}

The strict-witness-bounded dual feasible sublevel is compact.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualObjective_exists_isMinOn (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∃ (Z : MakingMeasurementsProjective.MatrixOperator model.space), (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ ∀ (W : MakingMeasurementsProjective.MatrixOperator model.space), (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model W g) → matrixSdpDualObjective model Z ≤ matrixSdpDualObjective model W

The paper-form canonical dual objective attains its minimum on the feasible set.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_isCompact (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : IsCompact {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model) | MatrixSdpCanonicalPrimalFeasible params model X}

The feasible set of the canonical primal SDP is compact.

theorem MIPStarRE.LDT.SelfImprovement.continuous_matrixSdpCanonicalPrimalObjective (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : Continuous fun (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) => (matrixSdpCanonicalObjectiveOperator params model * X).trace.re

The canonical primal objective is continuous.