Section 9 — Definitions #
The paper's SDP witnesses, the averaged point operators A_g = E_u A^u_{g(u)}, the SDP operators
built from them, and the pointwise and averaged sandwiched submeasurements
H^u_h = A^u_{h(u)} T_h A^u_{h(u)} and H_h = E_u H^u_h of thm:self-improvement: the
counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/SelfImprovement/Defs.lean in the port of
planning/c6b-plan.md (milestone M10, section "Port conventions").
A strategy is a SymStrat params 𝔓 K (Co/Test/StrategyCore.lean), and every operator of this
file is local: the primal witness T, the dual witness Z, the averaged point operators and the
sandwiched submeasurements live in the C*-algebra 𝔓 (the vendored Op ι). The vendored
matrix steps become generic ones: Matrix.PosSemidef.one.nonneg is zero_le_one, the
Matrix.sum_mul/Matrix.mul_sum regrouping is Finset.sum_mul/Finset.mul_sum, and the
sandwich bound is IsSelfAdjoint.conjugate_le_conjugate in 𝔓.
The vendored file imports MakingMeasurementsProjective/NaimarkCore.lean, which M8 did not port
(its finite-dimensional orthonormalization is replaced by T1). No NaimarkCore declaration is
named anywhere in SelfImprovement outside the matrix realization, which is not ported either;
what SelfImprovement reaches through that import is the ProjSubMeas/zeroProjSubMeas API and
orthonormalizationError. So this file imports the ported
Co/MakingMeasurementsProjective/Projectivization.lean in its place, which brings the former, and
through Co/MakingMeasurementsProjective/Statements.lean the vendored
MakingMeasurementsProjective/Defs.lean with the latter.
The classical declarations of the vendored file (the distinguished polynomial, the strict primal
weight, the add-in-u selections and the six error terms) are imported from it and named through
an explicit open MIPStarRE.LDT.SelfImprovement (…) list. The two threshold files of the
vendored directory, SelfImprovement/Theorems/Thresholds/Helper.lean and
SelfImprovement/Theorems/Thresholds/Final.lean, are wholly classical (scalar error
bookkeeping): they get no Co file, and the ported files that need them import them, as M3 imports
Preliminaries/Polynomials.lean.
Not ported #
sdpDistinguishedPolynomial: classical, imported.sdpStrictPrimalWeight: classical, imported.AddInUSelection: classical, imported.addInUSelectionPairs: classical, imported.selfImprovementVarianceError: classical, imported.addInUError: classical, imported.selfImprovementHelperError: classical, imported.selfImprovementOrthogonalizationError: classical, imported.selfImprovementDataProcessingError: classical, imported.selfImprovementError: classical, imported.sdpPrimalObjective: the real part of the matrix trace ofsdpPrimalObjectiveOperator; the model has no trace, and nothing in the vendored tree outside the matrix realization consumes it.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.tex
Paper origin: references/ldt-paper/self_improvement.tex:168-176
(\label{lem:sdp} strict feasible primal witness
T_g = (2 |\polyfunc{m}{q}{d}|)^{-1} I).
The constant strict primal effects have total mass (1/2)I. This is the
scalar identity behind the paper's strict feasible primal witness.
The paper's strict-feasible primal SDP witness
T_g = (2 |\polyfunc{m}{q}{d}|)^{-1} I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's uniform strict-feasible primal witness has total mass
(1 / 2) • I.
Paper origin: references/ldt-paper/self_improvement.tex:168-176
(\label{lem:sdp} strict feasible dual witness Z = 2I);
blueprint \label{lem:sdp-uniform-feasible-witness}.
The paper's strict-feasible dual SDP witness Z = 2I.
Equations
Instances For
The paper's strict-feasible dual witness 2I is positive.
The paper's strict-feasible dual witness dominates the identity: I ≤ 2I.
The averaged point operator A_g = E_u A^u_{g(u)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The averaged point operator A_g is positive.
The operator T_g A_g contributing to the primal SDP objective.
We take T to be a SubMeas rather than a full Measurement because the
paper's Section 9 primal only assumes ∑_g T_g ≤ I.
Equations
- MIPRE.LIDT.Co.SelfImprovement.sdpPrimalContributionOperator params strategy T g = T.outcome g * MIPRE.LIDT.Co.SelfImprovement.averagedPointOperator params strategy g
Instances For
The formal primal objective operator Σ_g T_g A_g.
Equations
- MIPRE.LIDT.Co.SelfImprovement.sdpPrimalObjectiveOperator params strategy T = ∑ g : MIPStarRE.LDT.Polynomial params, MIPRE.LIDT.Co.SelfImprovement.sdpPrimalContributionOperator params strategy T g
Instances For
The dual slack operator Z - A_g.
Equations
- MIPRE.LIDT.Co.SelfImprovement.sdpDualSlackOperator params strategy Z g = Z - MIPRE.LIDT.Co.SelfImprovement.averagedPointOperator params strategy g
Instances For
Dual feasibility already implies that the dual operator is positive, since every averaged
point operator A_g is positive.
The complementary-slackness equation T_g Z = T_g A_g.
Equations
- MIPRE.LIDT.Co.SelfImprovement.sdpComplementarySlacknessEquation params strategy T Z g = (T.outcome g * Z = T.outcome g * MIPRE.LIDT.Co.SelfImprovement.averagedPointOperator params strategy g)
Instances For
The pointwise sandwiched operator H^u_h = A^u_{h(u)} T_h A^u_{h(u)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sum of the pointwise sandwiched operators is bounded above by the identity: regrouped
by the value a = h(u), it is ∑_a A^u_a (∑_{h(u) = a} T_h) A^u_a ≤ ∑_a A^u_a = 1.
The pointwise sandwiched submeasurement H^u = {H^u_h}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The average of the total pointwise sandwiched operators is bounded by the identity.
The averaged sandwiched submeasurement H_h = E_u H^u_h.
Equations
- One or more equations did not get rendered due to their size.