Prove2Me

(24) — ρ∗=−r∗\rho^*=-r^*, μ∗\mu^* are feasible and optimal for the dual (22)

Proved
L0BnB.Duality.eq_24

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

dual-boundslagrangian-dualityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1strong-duality

Let X∈Rn×pX\in\mathbb R^{n\times p}, y∈Rny\in\mathbb R^n, λ0,λ2,M>0\lambda_0,\lambda_2,M>0 with λ0/λ2>M\sqrt{\lambda_0/\lambda_2}>M. Let β∗\beta^* be an optimal solution of the reduced relaxation (5), put r∗=y−Xβ∗r^*=y-X\beta^* and

ρ∗=−r∗,μi∗=1[∣βi∗∣=M](∣ρ∗TXi∣−λ0/M−λ2M),i∈[p].\rho^*=-r^*,\qquad \mu^*_i=\mathbb 1_{[|\beta^*_i|=M]}\big(|\rho^{*T}X_i|-\lambda_0/M-\lambda_2M\big),\quad i\in[p].

Then (ρ∗,μ∗)(\rho^*,\mu^*) is feasible for (22), that is ∣ρ∗TXi∣−μi∗≤λ0/M+λ2M|\rho^{*T}X_i|-\mu^*_i\le\lambda_0/M+\lambda_2M for every ii, and

h2(ρ∗,μ∗)=F(β∗).h_2(\rho^*,\mu^*)=F(\beta^*).

Together with weak duality this says that (ρ∗,μ∗)(\rho^*,\mu^*) is an optimal solution of (22) with no duality gap. The paper omits this proof ("follows along the lines similar to what was shown above").

Formalization Note Optimality of β∗\beta^* is a hypothesis; existence of a minimizer is not assumed.

Preamble
import Mathlib
import Definitions.Def_L0BnB_Duality_Dual
Formal statement
namespace L0BnB.Duality

/-- (24), Theorem 2, p. 14. Let `√(λ₀/λ₂) > M` and let `β*` be an optimal solution of (5). With
`r* = y − Xβ*`, the dual variables `ρ* = −r*` and `μ*ᵢ = 𝟙[|β*ᵢ| = M](|ρ*ᵀXᵢ| − λ₀/M − λ₂M)`
are feasible for (22) and attain the optimal value of (5): `h₂(ρ*, μ*) = L0BnB.Reduced.F(β*)`. -/
theorem eq_24 {n p : ℕ} (X : Matrix (Fin n) (Fin p) ℝ) (y : Fin n → ℝ)
    (lam0 lam2 M : ℝ) (hlam0 : 0 < lam0) (hlam2 : 0 < lam2) (hM : 0 < M)
    (hreg : M < Real.sqrt (lam0 / lam2))
    (βs : Fin p → ℝ) (hβs : βs ∈ L0BnB.Reduced.box p M)
    (hopt : ∀ β ∈ L0BnB.Reduced.box p M, L0BnB.Reduced.F X y lam0 lam2 M βs ≤ L0BnB.Reduced.F X y lam0 lam2 M β) :
    Feas22 X lam0 lam2 M (rhoStar X y βs) (muStar X y lam0 lam2 M βs) ∧
      h2 y M (rhoStar X y βs) (muStar X y lam0 lam2 M βs) = L0BnB.Reduced.F X y lam0 lam2 M βs := by sorry

end L0BnB.Duality
Source
Hazimeh, Mazumder, Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, p. 14, Theorem 2, (24); p. 31, Proof of Theorem 2, case √(λ0/λ2) > M
Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph