Section 9 — Matrix realization

Concrete finite-dimensional matrix realizations of the self-improvement SDP data.

References

• references/ldt-paper/self_improvement.tex

structure MIPStarRE.LDT.SelfImprovement.MatrixSdpRealization (params : Parameters) [FieldModel params.q] : Type (u + 1)

A concrete finite-dimensional matrix realization of the SDP data.

• space : MakingMeasurementsProjective.FiniteHilbertSpace
• state : MakingMeasurementsProjective.PositiveMatrixState self.space
• pointMeasurement : Point params → MakingMeasurementsProjective.MatrixSubmeasurement (Fq params) self.space

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpStrictPrimalSubmeasurement (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space

The matrix-level strict-feasible primal witness T_g = (2 |\polyfunc{m}{q}{d}|)^{-1} I.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpStrictPrimalSubmeasurement_sum_effect (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : ∑ g : Polynomial params, (matrixSdpStrictPrimalSubmeasurement params model).effect g = (1 / 2) • 1

The matrix-level strict-feasible primal witness has total mass (1/2) I.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpStrictDualWitness {params : Parameters} [FieldModel params.q] (model : MatrixSdpRealization params) : MakingMeasurementsProjective.MatrixOperator model.space

Paper origin: references/ldt-paper/self_improvement.tex:168-176 (\label{lem:sdp} strict feasible dual witness Z = 2I); blueprint \label{lem:sdp-matrix-feasible-bounds}.

The paper's matrix-level strict-feasible dual witness Z = 2I.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpStrictDualWitness model = 2 • 1

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpStrictDualWitness_nonneg {params : Parameters} [FieldModel params.q] (model : MatrixSdpRealization params) : 0 ≤ matrixSdpStrictDualWitness model

The matrix-level strict-feasible dual witness is positive semidefinite.

theorem MIPStarRE.LDT.SelfImprovement.one_le_matrixSdpStrictDualWitness {params : Parameters} [FieldModel params.q] (model : MatrixSdpRealization params) : 1 ≤ matrixSdpStrictDualWitness model

The matrix-level strict-feasible dual witness dominates the identity.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperatorContribution (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) (u : Point params) : MakingMeasurementsProjective.MatrixOperator model.space

The concrete operator A^u_{g(u)} entering the SDP average.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperatorContribution params model g u = (model.pointMeasurement u).effect (g.toFun u)

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) : MakingMeasurementsProjective.MatrixOperator model.space

The concrete averaged operator A_g = E_u A^u_{g(u)}.

This is defined through the project-wide distributional average averageOperatorOverDistribution so that the submeasurement averaging lemmas apply directly. The operator is used only in this matrix realization layer.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator_le_one (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) : matrixAveragedPointOperator params model g ≤ 1

The averaged point operator A_g is bounded by the identity.

theorem MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator_nonneg (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) : 0 ≤ matrixAveragedPointOperator params model g

The averaged point operator A_g is positive semidefinite.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpPrimalContributionOperator (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (g : Polynomial params) : MakingMeasurementsProjective.MatrixOperator model.space

The concrete primal contribution T_g A_g.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpPrimalContributionOperator params model T g = T.effect g * MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator params model g

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpPrimalObjective (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : Error

The concrete primal objective Σ_g Re Tr(T_g A_g).

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpDualObjective {params : Parameters} [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) : Error

The concrete dual objective Re Tr(Z).

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpDualObjective model Z = (Matrix.trace Z).re

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpDualSlackOperator (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (g : Polynomial params) : MakingMeasurementsProjective.MatrixOperator model.space

The concrete dual slack operator Z - A_g.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpDualSlackOperator params model Z g = Z - MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator params model g

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpStrictDualWitness_dualFeasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model (matrixSdpStrictDualWitness model) g

The matrix-level strict-feasible dual witness 2I dominates every averaged point operator.

theorem MIPStarRE.LDT.SelfImprovement.one_le_matrixSdpStrictDualWitness_dualSlack (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (g : Polynomial params) : 1 ≤ matrixSdpDualSlackOperator params model (matrixSdpStrictDualWitness model) g

For the strict dual witness Z = 2I, every paper dual slack Z - A_g dominates the identity.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpDualPositive_of_dualFeasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) : 0 ≤ Z

Dual feasibility already implies that the dual operator is positive semidefinite, since every averaged point operator A_g is positive.

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

Matrix-level record of the explicit feasible bounds used in the SDP argument.

The uniform primal family has total (1/2)I, while the dual witness 2I dominates the identity and is dual feasible. Positivity of the dual witness is derivable from dual feasibility and the positivity of the averaged point operators. These are the non-strict matrix inequalities currently recorded in Lean; the structure is not an optimality statement and does not include complementary slackness.

• primalTotalHalf : ∑ g : Polynomial params, T.effect g = (1 / 2) • 1
• dualDominatesIdentity : 1 ≤ Z
• dualFeasible (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model Z g
• dualSlackDominatesIdentity (g : Polynomial params) : 1 ≤ matrixSdpDualSlackOperator params model Z g

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpFeasibleBounds_canonical (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : MatrixSdpFeasibleBounds params model (matrixSdpStrictPrimalSubmeasurement params model) (matrixSdpStrictDualWitness model)

The canonical explicit matrix feasible bounds used in the SDP argument.