Section 9 — Canonical matrix SDP primal block form

This module contains the canonical block Hilbert space, diagonal-block operators, primal slack block, and extraction of paper primal submeasurements from feasible canonical primal matrices.

References

• references/ldt-paper/self_improvement.tex

@[reducible, inline]

abbrev MIPStarRE.LDT.SelfImprovement.MatrixSdpCanonicalBlockIndex (params : Parameters) [FieldModel params.q] : Type u_1

The block index set for the canonical primal SDP.

The some g blocks carry the primal operators T_g. The none block is the slack block S in the canonical equality constraint ∑_g T_g + S = I.

Equations

• MIPStarRE.LDT.SelfImprovement.MatrixSdpCanonicalBlockIndex params = Option (MIPStarRE.LDT.Polynomial params)

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockHilbertSpace (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : MakingMeasurementsProjective.FiniteHilbertSpace

The finite Hilbert space carrying the canonical block primal variable.

Equations

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

def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (b : MatrixSdpCanonicalBlockIndex params) : MakingMeasurementsProjective.MatrixOperator model.space

The diagonal block of a canonical primal matrix.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock params model X b i j = X (b, i) (b, j)

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

Projection onto one diagonal block of a canonical primal matrix, as a complex-linear map in the ambient block matrix.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlockLinearMap params model b = Matrix.submatrixLinearMap ℂ (fun (i : model.space.carrier) => (b, i)) fun (i : model.space.carrier) => (b, i)

@[simp]

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_zero (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (b : MatrixSdpCanonicalBlockIndex params) : matrixSdpCanonicalDiagonalBlock params model 0 b = 0

The diagonal-block projection sends the zero canonical matrix to zero.

@[simp]

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

The diagonal-block projection preserves addition.

@[simp]

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

The diagonal-block projection preserves negation.

@[simp]

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

The diagonal-block projection preserves subtraction.

@[simp]

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

The diagonal-block projection preserves complex scalar multiplication.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonalRingHom (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : (MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) →+* MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)

The ring homomorphism underlying the canonical block-diagonal construction.

The canonical SDP indexes its matrix space by (block, vector), while Mathlib's Matrix.blockDiagonalRingHom uses (vector, block). This map composes Mathlib's block-diagonal ring homomorphism with the canonical reindexing equivalence.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonalLinearMap (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : (MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) →ₗ[ℂ] MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)

The linear map underlying the canonical block-diagonal construction.

This is the linear counterpart of matrixSdpCanonicalBlockDiagonalRingHom. The construction is Mathlib's block-diagonal linear map followed by the canonical reindexing of the SDP block space.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : MakingMeasurementsProjective.MatrixOperator model.space

The operator-valued canonical equality constraint ∑_b X_{bb} = I.

The paper states the same constraint as the scalar family Tr(D_{ij}^† X) = b_{ij} for all matrix units D_{ij} and then identifies it with the operator equation ∑_b X_{bb} = I. This definition records the left-hand operator of that equivalent equation.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperatorLinearMap (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model) →ₗ[ℂ] MakingMeasurementsProjective.MatrixOperator model.space

The canonical equality-constraint operator as a complex-linear map.

Equations

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

@[simp]

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_zero (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : matrixSdpCanonicalConstraintOperator params model 0 = 0

The canonical equality-constraint operator sends zero to zero.

@[simp]

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

The canonical equality-constraint operator preserves addition.

@[simp]

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

The canonical equality-constraint operator preserves negation.

@[simp]

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

The canonical equality-constraint operator preserves subtraction.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_smul (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (c : ℂ) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : matrixSdpCanonicalConstraintOperator params model (c • X) = c • matrixSdpCanonicalConstraintOperator params model X

The canonical equality-constraint operator preserves complex scalar multiplication.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)

The block-diagonal matrix with prescribed diagonal blocks.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal params model B = (MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonalRingHom params model) B

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonalLinearMap_apply (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonalLinearMap params model) B = matrixSdpCanonicalBlockDiagonal params model B

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_eq_reindex_blockDiagonal (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : matrixSdpCanonicalBlockDiagonal params model B = (Matrix.reindex (Equiv.prodComm model.space.carrier (MatrixSdpCanonicalBlockIndex params)) (Equiv.prodComm model.space.carrier (MatrixSdpCanonicalBlockIndex params))) (Matrix.blockDiagonal B)

The canonical SDP block layout is the Mathlib block-diagonal layout after commuting the matrix-space index with the block index.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_zero (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : matrixSdpCanonicalBlockDiagonal params model 0 = 0

The canonical block-diagonal construction sends the zero family to the zero operator.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_apply (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (b c : MatrixSdpCanonicalBlockIndex params) (i j : model.space.carrier) : matrixSdpCanonicalBlockDiagonal params model B (b, i) (c, j) = if b = c then B b i j else 0

Entrywise form of the canonical block-diagonal matrix.

This is the old case-split presentation, now derived from Mathlib's Matrix.blockDiagonal through the index reordering used by matrixSdpCanonicalBlockDiagonal.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_one (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) : (matrixSdpCanonicalBlockDiagonal params model fun (x : MatrixSdpCanonicalBlockIndex params) => 1) = 1

The canonical block diagonal with identity on every block is the identity operator on the canonical block Hilbert space.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_add (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B D : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => B b + D b) = matrixSdpCanonicalBlockDiagonal params model B + matrixSdpCanonicalBlockDiagonal params model D

Addition of canonical block-diagonal operators is blockwise addition.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_neg (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => -B b) = -matrixSdpCanonicalBlockDiagonal params model B

Negation of canonical block-diagonal operators is blockwise negation.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_sub (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B D : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => B b - D b) = matrixSdpCanonicalBlockDiagonal params model B - matrixSdpCanonicalBlockDiagonal params model D

Subtraction of canonical block-diagonal operators is blockwise subtraction.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_smul (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (c : ℂ) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => c • B b) = c • matrixSdpCanonicalBlockDiagonal params model B

Scalar multiplication of canonical block-diagonal operators is blockwise scalar multiplication.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_sub_one (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : matrixSdpCanonicalBlockDiagonal params model B - 1 = matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => B b - 1

Subtracting the identity from a canonical block-diagonal operator subtracts the identity from each diagonal block.

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

A canonical block-diagonal operator is positive semidefinite when all of its diagonal matrix blocks are positive semidefinite.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_nonneg_iff (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : 0 ≤ matrixSdpCanonicalBlockDiagonal params model B ↔ ∀ (b : MatrixSdpCanonicalBlockIndex params), 0 ≤ B b

A canonical block-diagonal operator is positive semidefinite exactly when all of its diagonal matrix blocks are positive semidefinite.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_blockDiagonal (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (b : MatrixSdpCanonicalBlockIndex params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalBlockDiagonal params model B) b = B b

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_blockDiagonal (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : matrixSdpCanonicalConstraintOperator params model (matrixSdpCanonicalBlockDiagonal params model B) = ∑ b : MatrixSdpCanonicalBlockIndex params, B b

The canonical equality constraint of a block-diagonal matrix is the sum of its diagonal blocks.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_mul (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B D : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : matrixSdpCanonicalBlockDiagonal params model B * matrixSdpCanonicalBlockDiagonal params model D = matrixSdpCanonicalBlockDiagonal params model fun (b : MatrixSdpCanonicalBlockIndex params) => B b * D b

The product of two canonical block-diagonal operators is the canonical block-diagonal operator obtained by multiplying corresponding blocks.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonical_trace_eq_sum_diagonalBlock (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : Matrix.trace X = ∑ b : MatrixSdpCanonicalBlockIndex params, Matrix.trace (matrixSdpCanonicalDiagonalBlock params model X b)

The trace of a canonical block matrix is the sum of the traces of its diagonal blocks.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_trace_mul (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B D : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) : (matrixSdpCanonicalBlockDiagonal params model B * matrixSdpCanonicalBlockDiagonal params model D).trace = ∑ b : MatrixSdpCanonicalBlockIndex params, (B b * D b).trace

The trace pairing of two canonical block-diagonal operators is the sum of the trace pairings of their diagonal blocks.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_blockDiagonal_mul_left (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (b : MatrixSdpCanonicalBlockIndex params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalBlockDiagonal params model B * X) b = B b * matrixSdpCanonicalDiagonalBlock params model X b

The diagonal block of a product with a canonical block-diagonal operator on the left depends only on the corresponding diagonal block of the right factor.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalBlockDiagonal_trace_mul_left (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : (matrixSdpCanonicalBlockDiagonal params model B * X).trace = ∑ b : MatrixSdpCanonicalBlockIndex params, (B b * matrixSdpCanonicalDiagonalBlock params model X b).trace

The trace pairing of a canonical block-diagonal operator with an arbitrary canonical matrix depends only on the diagonal blocks of the latter.

This is the block calculation used in the converse direction of the canonical primal SDP identification: when the objective operator is block diagonal, the off-diagonal blocks of a feasible canonical matrix do not contribute to the objective value.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_mul_blockDiagonal_right (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (B : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space) (b : MatrixSdpCanonicalBlockIndex params) : matrixSdpCanonicalDiagonalBlock params model (X * matrixSdpCanonicalBlockDiagonal params model B) b = matrixSdpCanonicalDiagonalBlock params model X b * B b

The diagonal block of a product with a canonical block-diagonal operator on the right depends only on the corresponding diagonal block of the left factor.

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

The primal slack block S = I - ∑_g T_g.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSlackOperator params model T = 1 - ∑ g : MIPStarRE.LDT.Polynomial params, T.effect g

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSlackOperator_nonneg (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : 0 ≤ matrixSdpCanonicalSlackOperator params model T

The slack block of a matrix submeasurement is positive semidefinite.

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

The block family associated to the paper primal variable and its slack.

Equations

• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockFamily params model T none = MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSlackOperator params model T
• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockFamily params model T (some g) = T.effect g

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockFamily_none (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : matrixSdpCanonicalPrimalBlockFamily params model T none = matrixSdpCanonicalSlackOperator params model T

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockFamily_some (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (g : Polynomial params) : matrixSdpCanonicalPrimalBlockFamily params model T (some g) = T.effect g

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

The canonical block matrix associated to the paper primal submeasurement.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_primalBlockMatrix_some (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (g : Polynomial params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model T) (some g) = T.effect g

The polynomial diagonal blocks of the canonical primal matrix are the paper primal operators T_g.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_primalBlockMatrix_none (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model T) none = matrixSdpCanonicalSlackOperator params model T

The extra diagonal block of the canonical primal matrix is the slack operator I - ∑_g T_g.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockMatrix_nonneg (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : 0 ≤ matrixSdpCanonicalPrimalBlockMatrix params model T

The canonical block matrix associated to a paper primal submeasurement is positive semidefinite.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalConstraintOperator_primalBlockMatrix (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : matrixSdpCanonicalConstraintOperator params model (matrixSdpCanonicalPrimalBlockMatrix params model T) = 1

The canonical block matrix associated to a submeasurement satisfies the canonical equality constraint ∑_g T_g + S = I.

structure MIPStarRE.LDT.SelfImprovement.MatrixSdpCanonicalPrimalFeasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : Prop

Feasibility for the canonical primal block SDP: the block variable is positive semidefinite and satisfies the equality constraint X_{none,none} + ∑_g X_{gg} = I.

• nonnegative : 0 ≤ X

  The canonical primal matrix variable is positive semidefinite.

• constraintEqOne : matrixSdpCanonicalConstraintOperator params model X = 1

  The diagonal-block equality constraint holds.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalBlockMatrix_feasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) : MatrixSdpCanonicalPrimalFeasible params model (matrixSdpCanonicalPrimalBlockMatrix params model T)

A paper primal submeasurement determines a feasible point of the canonical block primal SDP by adjoining the slack block I - ∑_g T_g.

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

Every diagonal block X_{bb} of a positive canonical primal matrix is positive semidefinite.

This is the formal version of the paper's assertion that, from X ≥ 0, each principal block X_{ii} is positive.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_sum_diagonalBlock_some_le_one (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)} (hX : MatrixSdpCanonicalPrimalFeasible params model X) : ∑ g : Polynomial params, matrixSdpCanonicalDiagonalBlock params model X (some g) ≤ 1

The polynomial diagonal blocks of a feasible canonical primal matrix form a submeasurement total.

The canonical constraint gives X_{none,none} + ∑_g X_{gg} = I; since the slack block X_{none,none} is positive, the polynomial blocks satisfy ∑_g X_{gg} ≤ I.

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalExtractedPrimalSubmeasurement (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space

The paper primal submeasurement extracted from a feasible canonical primal matrix by setting T_g = X_{gg} on the polynomial blocks.

Equations

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

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalExtractedPrimalSubmeasurement_effect (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (g : Polynomial params) : (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX).effect g = matrixSdpCanonicalDiagonalBlock params model X (some g)

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSlackOperator_extractedPrimalSubmeasurement (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : matrixSdpCanonicalSlackOperator params model (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX) = matrixSdpCanonicalDiagonalBlock params model X none

The slack block of the submeasurement extracted from a feasible canonical matrix is the original canonical slack diagonal block.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_primalBlockMatrix_extracted_some (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (g : Polynomial params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX)) (some g) = matrixSdpCanonicalDiagonalBlock params model X (some g)

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_primalBlockMatrix_extracted_none (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX)) none = matrixSdpCanonicalDiagonalBlock params model X none

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_primalBlockMatrix_extracted (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (b : MatrixSdpCanonicalBlockIndex params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX)) b = matrixSdpCanonicalDiagonalBlock params model X b

Replacing a feasible canonical matrix by the canonical block matrix of its extracted paper submeasurement preserves every diagonal block.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalPrimalFeasible_extracts_submeasurement (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : ∃ (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space), ∀ (g : Polynomial params), T.effect g = matrixSdpCanonicalDiagonalBlock params model X (some g)

A feasible canonical primal matrix determines a paper primal submeasurement with effects T_g = X_{gg}.