Prove2Me

Theorem 2 — Lagrangian duals of the reduced relaxation (5) and their optimal dual variables

Proved
L0BnB.Duality.theorem_2

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

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

Let X∈Rn×pX\in\mathbb R^{n\times p} with columns XiX_i, y∈Rny\in\mathbb R^n and λ0,λ2,M>0\lambda_0,\lambda_2,M>0. Let β∗\beta^* be an optimal solution of the reduced relaxation

min⁡β∈Rp F(β)=12∥y−Xβ∥22+∑i∈[p]ψ(βi;λ0,λ2,M)s.t.∥β∥∞≤M,(5)\min_{\beta\in\mathbb R^p}\ F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M)\quad\text{s.t.}\quad\|\beta\|_\infty\le M,\tag{5}

and let r∗=y−Xβ∗r^*=y-X\beta^*.

  1. If λ0/λ2≤M\sqrt{\lambda_0/\lambda_2}\le M, the problem
max⁡α∈Rn,γ∈Rph1(α,γ)=−12∥α∥22−αTy−∑i∈[p]([(αTXi−γi)24λ2−λ0]++M∣γi∣)(20)\max_{\alpha\in\mathbb R^n,\gamma\in\mathbb R^p} h_1(\alpha,\gamma)=-\tfrac12\|\alpha\|_2^2-\alpha^Ty-\sum_{i\in[p]}\Big(\Big[\frac{(\alpha^TX_i-\gamma_i)^2}{4\lambda_2}-\lambda_0\Big]_+ + M|\gamma_i|\Big)\tag{20}

is a dual of (5): h1(α,γ)≤F(β)h_1(\alpha,\gamma)\le F(\beta) for all α,γ\alpha,\gamma and all feasible β\beta. Its optimal dual variables are α∗=−r∗\alpha^*=-r^* and γi∗=1[∣βi∗∣=M](α∗TXi−2Mλ2 sign(α∗TXi))\gamma^*_i=\mathbb 1_{[|\beta^*_i|=M]}(\alpha^{*T}X_i-2M\lambda_2\,\mathrm{sign}(\alpha^{*T}X_i)), which satisfy h1(α∗,γ∗)=F(β∗)h_1(\alpha^*,\gamma^*)=F(\beta^*). 2. If λ0/λ2>M\sqrt{\lambda_0/\lambda_2}>M, the problem

max⁡ρ∈Rn,μ∈Rph2(ρ,μ)=−12∥ρ∥22−ρTy−M∥μ∥1s.t.∣ρTXi∣−μi≤λ0/M+λ2M, i∈[p](22)\max_{\rho\in\mathbb R^n,\mu\in\mathbb R^p} h_2(\rho,\mu)=-\tfrac12\|\rho\|_2^2-\rho^Ty-M\|\mu\|_1\quad\text{s.t.}\quad |\rho^TX_i|-\mu_i\le\lambda_0/M+\lambda_2M,\ i\in[p]\tag{22}

is a dual of (5): h2(ρ,μ)≤F(β)h_2(\rho,\mu)\le F(\beta) for all feasible (ρ,μ)(\rho,\mu) and all feasible β\beta. Its optimal dual variables are ρ∗=−r∗\rho^*=-r^* and μi∗=1[∣βi∗∣=M](∣ρ∗TXi∣−λ0/M−λ2M)\mu^*_i=\mathbb 1_{[|\beta^*_i|=M]}(|\rho^{*T}X_i|-\lambda_0/M-\lambda_2M), which are feasible for (22) and satisfy h2(ρ∗,μ∗)=F(β∗)h_2(\rho^*,\mu^*)=F(\beta^*).

The closed-form dual variables are what make cheap dual bounds possible in the paper's branch-and-bound method: at an inexact primal solution β^\hat\beta, the choice α^=−r^\hat\alpha=-\hat r imitates (23) and yields a valid lower bound for pruning.

Formalization Note "A dual of (5) is given by (20)" with optimal variables (23) is formalized as weak duality over all dual points together with equality of the dual value at (α∗,γ∗)(\alpha^*,\gamma^*) and the primal value at β∗\beta^*; this is strong duality with an explicit maximizer. Uniqueness of the dual optimum is not claimed. sign is Real.sign (sign(0)=0\mathrm{sign}(0)=0), which is never evaluated at 00 on an index with ∣βi∗∣=M|\beta^*_i|=M. Optimality of β∗\beta^* is a hypothesis.

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

/-- Theorem 2, pp. 13–14. Let `β*` be an optimal solution of (5) and `r* = y − Xβ*`.
1. If `√(λ₀/λ₂) ≤ M`, then (20) is a dual of (5): `h₁(α, γ) ≤ L0BnB.Reduced.F(β)` for all `α ∈ ℝⁿ`, `γ ∈ ℝᵖ`
   and all `β` feasible for (5); and the dual variables (23), `α* = −r*`,
   `γ*ᵢ = 𝟙[|β*ᵢ| = M](α*ᵀXᵢ − 2Mλ₂ sign(α*ᵀXᵢ))`, are optimal: `h₁(α*, γ*) = L0BnB.Reduced.F(β*)`.
2. If `√(λ₀/λ₂) > M`, then (22) is a dual of (5): `h₂(ρ, μ) ≤ L0BnB.Reduced.F(β)` for all `(ρ, μ)` feasible
   for (22) and all `β` feasible for (5); and the dual variables (24), `ρ* = −r*`,
   `μ*ᵢ = 𝟙[|β*ᵢ| = M](|ρ*ᵀXᵢ| − λ₀/M − λ₂M)`, are feasible for (22) and optimal:
   `h₂(ρ*, μ*) = L0BnB.Reduced.F(β*)`. -/
theorem theorem_2 {n p : ℕ} (X : Matrix (Fin n) (Fin p) ℝ) (y : Fin n → ℝ)
    (lam0 lam2 M : ℝ) (hlam0 : 0 < lam0) (hlam2 : 0 < lam2) (hM : 0 < M)
    (β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 β) :
    (Real.sqrt (lam0 / lam2) ≤ M →
      (∀ (α : Fin n → ℝ) (γ : Fin p → ℝ), ∀ β ∈ L0BnB.Reduced.box p M,
        h1 X y lam0 lam2 M α γ ≤ L0BnB.Reduced.F X y lam0 lam2 M β) ∧
      h1 X y lam0 lam2 M (alphaStar X y βs) (gammaStar X y lam2 M βs) =
        L0BnB.Reduced.F X y lam0 lam2 M βs) ∧
    (M < Real.sqrt (lam0 / lam2) →
      (∀ (ρ : Fin n → ℝ) (μ : Fin p → ℝ), Feas22 X lam0 lam2 M ρ μ → ∀ β ∈ L0BnB.Reduced.box p M,
        h2 y M ρ μ ≤ 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, pp. 13–14, Theorem 2, (20)–(24); pp. 30–31, Proof of Theorem 2
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