Section 9 — Definitions

This file exposes the paper's SDP witnesses, the add-in-u transfer identity, and the non-projective/projective self-improvement outputs through explicit named constructions and error terms.

References

• references/ldt-paper/self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpDistinguishedPolynomial (params : Parameters) [FieldModel params.q] : Polynomial params

The zero polynomial used as the distinguished polynomial block in canonical SDP completion arguments.

Equations

• MIPStarRE.LDT.SelfImprovement.sdpDistinguishedPolynomial params = { poly := 0, lowIndividualDegree := ⋯ }

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpStrictPrimalWeight (params : Parameters) [FieldModel params.q] : Error

The paper's strict-feasibility weight 1 / (2 |\polyfunc{m}{q}{d}|).

Equations

• MIPStarRE.LDT.SelfImprovement.sdpStrictPrimalWeight params = 1 / (2 * ↑(Fintype.card (MIPStarRE.LDT.Polynomial params)))

theorem MIPStarRE.LDT.SelfImprovement.sdpStrictPrimalConstantSum {ι : Type u_1} [DecidableEq ι] (params : Parameters) [FieldModel params.q] : ∑ x : Polynomial params, sdpStrictPrimalWeight params • 1 = (1 / 2) • 1

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.

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpStrictPrimalSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] : SubMeas (Polynomial params) ι

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.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.sdpStrictPrimalSubMeas_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] : (sdpStrictPrimalSubMeas params).total = (1 / 2) • 1

The paper's uniform strict-feasible primal witness has total mass (1 / 2) • I.

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpStrictDualWitness {ι : Type u_1} [DecidableEq ι] : Quantum.Op ι

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

• MIPStarRE.LDT.SelfImprovement.sdpStrictDualWitness = 2 • 1

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.sdpStrictDualWitness_nonneg {ι : Type u_2} [Finite ι] [DecidableEq ι] : 0 ≤ sdpStrictDualWitness

The paper's strict-feasible dual witness 2I is positive semidefinite.

theorem MIPStarRE.LDT.SelfImprovement.one_le_sdpStrictDualWitness {ι : Type u_2} [Finite ι] [DecidableEq ι] : 1 ≤ sdpStrictDualWitness

The paper's strict-feasible dual witness dominates the identity: I ≤ 2I.

noncomputable def MIPStarRE.LDT.SelfImprovement.averagedPointOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (g : Polynomial params) : Quantum.Op ι

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.

theorem MIPStarRE.LDT.SelfImprovement.averagedPointOperator_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (g : Polynomial params) : 0 ≤ averagedPointOperator params strategy g

The averaged point operator A_g is positive semidefinite.

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpPrimalContributionOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (g : Polynomial params) : Quantum.Op ι

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

• MIPStarRE.LDT.SelfImprovement.sdpPrimalContributionOperator params strategy T g = T.outcome g * MIPStarRE.LDT.SelfImprovement.averagedPointOperator params strategy g

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpPrimalObjectiveOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Quantum.Op ι

The formal primal objective operator Σ_g T_g A_g.

Equations

• MIPStarRE.LDT.SelfImprovement.sdpPrimalObjectiveOperator params strategy T = ∑ g : MIPStarRE.LDT.Polynomial params, MIPStarRE.LDT.SelfImprovement.sdpPrimalContributionOperator params strategy T g

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpPrimalObjective {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The primal objective value Σ_g Tr(T_g A_g).

Equations

• MIPStarRE.LDT.SelfImprovement.sdpPrimalObjective params strategy T = (Matrix.trace (MIPStarRE.LDT.SelfImprovement.sdpPrimalObjectiveOperator params strategy T)).re

noncomputable def MIPStarRE.LDT.SelfImprovement.sdpDualSlackOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (Z : Quantum.Op ι) (g : Polynomial params) : Quantum.Op ι

The dual slack operator Z - A_g.

Equations

• MIPStarRE.LDT.SelfImprovement.sdpDualSlackOperator params strategy Z g = Z - MIPStarRE.LDT.SelfImprovement.averagedPointOperator params strategy g

theorem MIPStarRE.LDT.SelfImprovement.sdpDualPositive_of_dualFeasible {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (Z : Quantum.Op ι) (hdual : ∀ (g : Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) : 0 ≤ Z

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

def MIPStarRE.LDT.SelfImprovement.sdpComplementarySlacknessEquation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (g : Polynomial params) : Prop

The complementary-slackness equation T_g Z = T_g A_g.

Equations

• MIPStarRE.LDT.SelfImprovement.sdpComplementarySlacknessEquation params strategy T Z g = (T.outcome g * Z = T.outcome g * MIPStarRE.LDT.SelfImprovement.averagedPointOperator params strategy g)

@[reducible, inline]

abbrev MIPStarRE.LDT.SelfImprovement.AddInUSelection (params : Parameters) [FieldModel params.q] (Outcome : Type u_2) : Type (max u_3 u_2)

A point-indexed selection of outcome/polynomial pairs used in lem:add-in-u.

Equations

• MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome = (MIPStarRE.LDT.Point params → Set (Outcome × MIPStarRE.LDT.Polynomial params))

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectionPairs {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (S : AddInUSelection params Outcome) (u : Point params) : Finset (Outcome × Polynomial params)

The finite set of selected outcome/polynomial pairs at a point u.

Equations

• MIPStarRE.LDT.SelfImprovement.addInUSelectionPairs params S u = {ah : Outcome × MIPStarRE.LDT.Polynomial params | ah ∈ S u}

noncomputable def MIPStarRE.LDT.SelfImprovement.sandwichedPolynomialOutcomeOperatorAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (h : Polynomial params) : Quantum.Op ι

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.

noncomputable def MIPStarRE.LDT.SelfImprovement.sandwichedPolynomialSubMeasAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) : SubMeas (Polynomial params) ι

The pointwise sandwiched submeasurement H^u = {H^u_h}.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.averagedSandwichedPolynomialSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : SubMeas (Polynomial params) ι

The averaged sandwiched submeasurement H_h = E_u H^u_h.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The variance error entering lem:add-in-u.

Equations

• MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta = MIPStarRE.LDT.GlobalVariance.globalVarianceOfPointsError params eps delta

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The error term in lem:add-in-u.

Equations

• MIPStarRE.LDT.SelfImprovement.addInUError params eps delta = 4 * Real.rpow (MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta) (1 / 2)

noncomputable def MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The quantitative error from lem:self-improvement-helper.

Equations

• MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta = 100 * ↑params.m * (Real.rpow eps (1 / 2) + Real.rpow delta (1 / 2) + Real.rpow (↑params.d / ↑params.q) (1 / 2))

noncomputable def MIPStarRE.LDT.SelfImprovement.selfImprovementOrthogonalizationError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The orthogonalization error applied to the helper output.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The postprocessed error after projecting the helper output.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.selfImprovementError (params : Parameters) [FieldModel params.q] (eps delta : Error) : Error

The quantitative error from thm:self-improvement.

Equations

• MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta = MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError params eps delta 0