Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.SelfImprovement.MatrixRealization.Canonical.Witness

Section 9 — Canonical matrix SDP witnesses #

This module contains the optimal-witness structures extracted from the canonical matrix SDP. The preceding canonical module proves the block-diagonal algebra, including the dual slack identities and saturation of the slack block. This file records the paper-form optimal pair and the measurement witnesses used by the self-improvement comparison.

References #

source
structure MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (Z : MakingMeasurementsProjective.MatrixOperator model.space) :
Prop

Paper origin: references/ldt-paper/self_improvement.tex:82-88 (\label{lem:sdp}, \label{eq:slater}); docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex (SDP gap).

Matrix-level witness for an optimal SDP pair.

Instances For
    source
    structure MIPStarRE.LDT.SelfImprovement.MatrixSdpStatementWithSlackness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) :
    Prop

    Paper origin: references/ldt-paper/self_improvement.tex:82-181 (\label{lem:sdp}), with complementary slackness from eq:complementary-slackness at line 179; matrix realization of SdpStatementWithSlackness.

    Matrix-level statement of the strong-duality output for the SDP.

    This is the concrete matrix analogue of SdpStatementWithSlackness: it does not assert that the explicit strict feasible witnesses are optimal. Instead it records the kind of optimal witness obtained from the paper's Slater/strong-duality argument. The feasible primal variables in the canonical SDP remain submeasurements; this statement stores the selected saturated optimal witness as a complete matrix measurement.

    Grounded by: #1230.

    Instances For
      source
      def MIPStarRE.LDT.SelfImprovement.matrixSdpComplementarySlacknessEquation (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (g : Polynomial params) :
      Prop

      The concrete complementary-slackness equation T_g Z = T_g A_g.

      Equations
      Instances For
        source
        theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness.dualPositive {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} {T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space} {Z : MakingMeasurementsProjective.MatrixOperator model.space} (h : MatrixSdpOptimalWitness params model T Z) :
        0 ≤ Z

        The dual operator in an optimal matrix SDP witness is positive semidefinite. This follows from dual feasibility, because the averaged point operators are positive.

        source
        noncomputable def MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness.primalMeasurement {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} {T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space} {Z : MakingMeasurementsProjective.MatrixOperator model.space} (h : MatrixSdpOptimalWitness params model T Z) :
        MakingMeasurementsProjective.MatrixMeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space

        An optimal matrix SDP witness whose primal total is the identity determines a complete matrix measurement.

        Equations
        Instances For
          source
          @[simp]
          theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness.primalMeasurement_effect {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} {T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space} {Z : MakingMeasurementsProjective.MatrixOperator model.space} (h : MatrixSdpOptimalWitness params model T Z) (g : Polynomial params) :
          h.primalMeasurement.effect g = T.effect g
          source
          theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness.complementarySlacknessEquation {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} {T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space} {Z : MakingMeasurementsProjective.MatrixOperator model.space} (h : MatrixSdpOptimalWitness params model T Z) (g : Polynomial params) :
          matrixSdpComplementarySlacknessEquation params model T Z g

          The stored complementary-slackness equation, expressed through the named matrix-level predicate.

          source
          theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpStatementWithSlackness.exists_measurement_witness {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} (h : MatrixSdpStatementWithSlackness params model) :
          ∃ (T : MakingMeasurementsProjective.MatrixMeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (Z : MakingMeasurementsProjective.MatrixOperator model.space), 0 ≤ Z ∧ (∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) ∧ matrixSdpPrimalObjective params model T.toSubmeasurement = matrixSdpDualObjective model Z ∧ ∀ (g : Polynomial params), T.effect g * Z = T.effect g * matrixAveragedPointOperator params model g

          A matrix strong-duality statement gives a complete primal measurement, a dual operator, dual feasibility, equality of objective values, and the complementary-slackness equations in the displayed T_g Z = T_g A_g form.