Finite conic-duality separation lemmas

This module contains the product-space part of the finite-dimensional conic duality argument used by the Section 9 SDP. A separator on a product space E × ℝ decomposes into a constraint-coordinate functional and an objective coefficient. If the separator is nonnegative on a conic image and negative at a point with the same constraint coordinate but larger objective coordinate, then the objective coefficient is negative. After normalizing by this negative coefficient one obtains the functional dual bound.

The matrix trace-pairing representation and the paper-form SDP witness remain in the Section 9 matrix-realization layer.

References

• references/ldt-paper/self_improvement.tex
• docs/reports/issue-2386-finite-sdp-duality-theorem-design.md

noncomputable def MIPStarRE.Quantum.conicSeparatorConstraintFunctional {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) : StrongDual ℝ E

The constraint-coordinate part of a separator on a product space.

Equations

• MIPStarRE.Quantum.conicSeparatorConstraintFunctional φ = φ ∘SL ContinuousLinearMap.inl ℝ E ℝ

noncomputable def MIPStarRE.Quantum.conicSeparatorObjectiveCoefficient {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) : ℝ

The objective-coordinate coefficient of a separator on a product space.

Equations

• MIPStarRE.Quantum.conicSeparatorObjectiveCoefficient φ = (φ ∘SL ContinuousLinearMap.inr ℝ E ℝ) 1

theorem MIPStarRE.Quantum.conicSeparator_decompose {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) (y : E) (t : ℝ) : φ (y, t) = (conicSeparatorConstraintFunctional φ) y + t * conicSeparatorObjectiveCoefficient φ

A separator on E × ℝ is the sum of its constraint-coordinate part and objective-coordinate part.

theorem MIPStarRE.Quantum.conicSeparatorObjectiveCoefficient_neg_of_above {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {C : Set (E × ℝ)} (φ : StrongDual ℝ (E × ℝ)) {y : E} {s t : ℝ} (hφ : ∀ z ∈ C, 0 ≤ φ z) (hys : (y, s) ∈ C) (hyt : φ (y, t) < 0) (hst : s < t) : conicSeparatorObjectiveCoefficient φ < 0

If a separator is nonnegative on a conic image point (y, s) and negative at (y, t) with s < t, then its objective-coordinate coefficient is negative.

noncomputable def MIPStarRE.Quantum.conicNormalizedSeparatorFunctional {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) : StrongDual ℝ E

The normalized constraint-coordinate functional associated to a separator.

This definition is useful when the objective-coordinate coefficient is known to be negative.

Equations

• MIPStarRE.Quantum.conicNormalizedSeparatorFunctional φ = (-MIPStarRE.Quantum.conicSeparatorObjectiveCoefficient φ)⁻¹ • MIPStarRE.Quantum.conicSeparatorConstraintFunctional φ

@[simp]

theorem MIPStarRE.Quantum.conicNormalizedSeparatorFunctional_apply {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) (y : E) : (conicNormalizedSeparatorFunctional φ) y = (-conicSeparatorObjectiveCoefficient φ)⁻¹ * (conicSeparatorConstraintFunctional φ) y

theorem MIPStarRE.Quantum.conicObjective_le_normalizedSeparator_of_mem {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [TopologicalSpace F] [AddCommMonoid F] [Module ℝ F] (A : E →L[ℝ] F) (c : E →L[ℝ] ℝ) {C : Set (F × ℝ)} (φ : StrongDual ℝ (F × ℝ)) (hφ : ∀ z ∈ C, 0 ≤ φ z) (hcoeff : conicSeparatorObjectiveCoefficient φ < 0) (x : E) (hx : (A x, c x) ∈ C) : c x ≤ (conicNormalizedSeparatorFunctional φ) (A x)

A separator that is nonnegative on a conic image gives a normalized functional dual bound on any point whose constraint-objective image lies in that conic image.

theorem MIPStarRE.Quantum.conicFunctionalDualFeasible_normalizedSeparator {F : Type u_1} [TopologicalSpace F] [AddCommMonoid F] [Module ℝ F] {C : Set (F × ℝ)} (φ : StrongDual ℝ (F × ℝ)) (hφ : ∀ z ∈ C, 0 ≤ φ z) (hcoeff : conicSeparatorObjectiveCoefficient φ < 0) (z : F × ℝ) : z ∈ C → z.2 ≤ (conicNormalizedSeparatorFunctional φ) z.1

The normalized constraint functional associated to a separator is feasible for the functional dual problem of the conic image.

theorem MIPStarRE.Quantum.conicNormalizedSeparatorFunctional_lt_of_sep {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (φ : StrongDual ℝ (E × ℝ)) {y : E} {t : ℝ} (hsep : φ (y, t) < 0) (hcoeff : conicSeparatorObjectiveCoefficient φ < 0) : (conicNormalizedSeparatorFunctional φ) y < t

If a separator is negative at (y, t), then its normalized constraint-coordinate functional is below t at y.

theorem MIPStarRE.Quantum.conic_primalValue_eq_dualValue_of_fiber_max_dual_min {F : Type u_1} [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C : ProperCone ℝ (F × ℝ)) {y : F} {p d : ℝ} (hprimalMem : (y, p) ∈ C) (hprimalMax : ∀ {t : ℝ}, (y, t) ∈ C → t ≤ p) (hdualMin : ∀ (ψ : StrongDual ℝ F), (∀ z ∈ C, z.2 ≤ ψ z.1) → d ≤ ψ y) (hweak : p ≤ d) : p = d

A functional conic zero-gap theorem.

Let C be a closed conic image in F × ℝ. Suppose that, on the fiber over y, the value p lies in C and is maximal among all objective coordinates in that fiber. Suppose also that d is minimal among all continuous real-linear functionals ψ satisfying the functional dual inequalities t ≤ ψ y' for every (y', t) ∈ C. If weak duality gives p ≤ d, then the attained primal and dual values are equal.

This is the product-space separation argument behind finite-dimensional conic duality. It deliberately records the closed-image fiber condition through the maximality hypothesis, rather than assuming that fiber recovery is automatic.