Prove2Me

(45) — the minimizer of DiD_i on ∣βi∣≤λ0/λ2|\beta_i|\le\sqrt{\lambda_0/\lambda_2}

Proved
L0BnB.Duality.eq_45

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

lagrangian-dualityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1reverse-huber

Let λ0,λ2>0\lambda_0,\lambda_2>0, let a∈Ra\in\mathbb R (standing for αTXi\alpha^TX_i) and η≥0\eta\ge 0 (a multiplier ηi\eta_i), and let D(b)=ψ1(b;λ0,λ2)+ab+η∣b∣D(b)=\psi_1(b;\lambda_0,\lambda_2)+ab+\eta|b|. Set

β~={0if 2λ0λ2+η−∣a∣≥0,−λ0/λ2 sign(a)otherwise.\tilde\beta=\begin{cases}0 & \text{if } 2\sqrt{\lambda_0\lambda_2}+\eta-|a|\ge 0,\\ -\sqrt{\lambda_0/\lambda_2}\,\mathrm{sign}(a) & \text{otherwise.}\end{cases}

Then ∣β~∣≤λ0/λ2|\tilde\beta|\le\sqrt{\lambda_0/\lambda_2} and

D(β~)≤D(b)for every b with ∣b∣≤λ0/λ2.D(\tilde\beta)\le D(b)\qquad\text{for every } b \text{ with } |b|\le\sqrt{\lambda_0/\lambda_2}.

This is Case 1 of the inner minimization in the proof of Theorem 2: on this interval ψ1(b)=2λ0λ2∣b∣\psi_1(b)=2\sqrt{\lambda_0\lambda_2}|b|, so DD is piecewise linear.

Formalization Note The paper's "argmin" is stated as membership in the interval plus minimality over it; uniqueness is not claimed. η≥0\eta\ge 0 is the sign constraint of the multipliers in (43). sign is Real.sign; in the second case ∣a∣>2λ0λ2>0|a|>2\sqrt{\lambda_0\lambda_2}>0, so sign(0) does not arise there.

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

/-- (45), proof of Theorem 2, p. 31 (Case 1: `|βᵢ| ≤ √(λ₀/λ₂)`). For `a = αᵀXᵢ` and `η = ηᵢ ≥ 0`,
the point `β̃*ᵢ` of (45) lies in `[−√(λ₀/λ₂), √(λ₀/λ₂)]` and minimizes
`Dᵢ(βᵢ) = ψ₁(βᵢ; λ₀, λ₂) + a βᵢ + η|βᵢ|` over that interval. -/
theorem eq_45 (lam0 lam2 a η : ℝ) (hlam0 : 0 < lam0) (hlam2 : 0 < lam2) (hη : 0 ≤ η) :
    betaTilde45 lam0 lam2 a η ∈ Set.Icc (-Real.sqrt (lam0 / lam2)) (Real.sqrt (lam0 / lam2)) ∧
      ∀ b ∈ Set.Icc (-Real.sqrt (lam0 / lam2)) (Real.sqrt (lam0 / lam2)),
        D lam0 lam2 a η (betaTilde45 lam0 lam2 a η) ≤ D lam0 lam2 a η b := 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. 31, Proof of Theorem 2, Case 1, (45)
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