Pareto optimality via scalarization

Proved

ConvexOptimization.scalarization_sufficient_pareto

by Shuze Chen · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexoptimizationdualitykkt

Scalarization produces Pareto optimal points.

Let $X \subseteq \mathbb{R}^n$ and let $f : \mathbb{R}^n \to \mathbb{R}^{k}$ be a vector objective with components $f_1,\dots,f_k$ . Fix weights $\lambda \in \mathbb{R}^{k}$ with $\lambda_i > 0$ for every $i$ , and suppose $x^{\star} \in X$ minimizes the scalarized objective:

\sum_{i=1}^{k} \lambda_i f_i(x^{\star}) \;\le\; \sum_{i=1}^{k}\lambda_i f_i(y) \qquad \text{for every } y \in X .

Then $x^{\star}$ is Pareto optimal for $f$ : there is no $y \in X$ with $f_i(y) \le f_i(x^{\star})$ for all $i$ and $f(y) \ne f(x^{\star})$ — no feasible point improves some component without worsening another.

Scalarization is the standard device for reducing multicriterion optimization to the single-objective theory of this mission: choosing strictly positive weights and solving one ordinary problem yields a Pareto point, and sweeping the weights traces out a family of them. Strict positivity is essential — with a zero weight the minimizer may be dominated in the ignored coordinate.

Formalization Note The vector objective is a function into Fin k → ℝ; domination is expressed as componentwise $\le$ together with $f(y) \ne f(x^{\star})$ as functions, and the conclusion is the negation of an existential. No convexity of $X$ or of the components is needed for this direction. Source: B&V §4.7.4, p. 178.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.scalarization_sufficient_pareto {n k : ℕ}
    (X : Set (EuclideanSpace ℝ (Fin n)))
    (f : EuclideanSpace ℝ (Fin n) → Fin k → ℝ)
    (lam : Fin k → ℝ) (hlam : ∀ i, 0 < lam i)
    (xs : EuclideanSpace ℝ (Fin n)) (hxs : xs ∈ X)
    (hmin : ∀ y ∈ X, ∑ i, lam i * f xs i ≤ ∑ i, lam i * f y i) :
    ¬∃ y ∈ X, (∀ i, f y i ≤ f xs i) ∧ f y ≠ f xs := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 178, §4.7.4 (scalarization; finding Pareto optimal points by minimizing a positively weighted sum)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem. Fix implicit natural numbers $n$ and $k$ (either may be $0$ ), a set $X \subseteq \mathbb{R}^n$ (no convexity assumed), a vector-valued objective $f : \mathbb{R}^n \to \mathbb{R}^k$ (i.e. $k$ scalar components $f_i$ ), weights $\lambda \in \mathbb{R}^k$ with $\lambda_i > 0$ strictly for every $i$ , and a point $x_s \in X$ such that $\sum_i \lambda_i f_i(x_s) \le \sum_i \lambda_i f_i(y)$ for every $y \in X$ (i.e. $x_s$ minimizes the $\lambda$ -weighted sum over $X$ ; non-strict inequality). The conclusion is a negation: there does not exist $y \in X$ such that both $f_i(y) \le f_i(x_s)$ for every $i$ (componentwise, non-strict) and $f(y) \ne f(x_s)$ (the two vectors of values differ in at least one component). In other words, no point of $X$ weakly dominates $x_s$ in every component while differing from it in some component. Note the comparison $f(y) \ne f(x_s)$ is between the value vectors, not between the points $y$ and $x_s$ . Edge cases: if $k = 0$ the weight hypothesis is vacuous, all value vectors are equal (there is only one function $\mathrm{Fin}\,0 \to \mathbb{R}$ ), so the conclusion holds vacuously; if $X = \{x_s\}$ the conclusion is likewise immediate.

Human review

Endorsed by Community (Bot) · Aug 12, 2026
Endorsed by Shuze Chen · Aug 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph