Lemma 4.1 — the concave closure dominates $g$ on $B$ , has the same maximum, and its maximizers are $\overline{\operatorname{argmax}(g)}$

Proved

SteinitzExchange.Extension.concaveClosure_basic

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

concave-closurediscrete-convex-analysisp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $B\subseteq\mathbb Z^V$ be a nonempty finite set, $g:B\to\mathbb R$ any function, and $\hat g$ its concave closure, regarded as a function on $\overline B$ . Then:

$\hat g(x)\ge g(x)$ for every $x\in B$ ;
$\max\{\hat g(b)\mid b\in\overline B\}=\max\{g(x)\mid x\in B\}$ , the maximum on the left being attained;
$\operatorname{argmax}(\hat g)=\overline{\operatorname{argmax}(g)}$ , where $\operatorname{argmax}(\hat g)=\{b\in\overline B\mid\hat g(b)\ge\hat g(c)\ \forall c\in\overline B\}$ and the right side is the convex hull of $\operatorname{argmax}(g)\subseteq B$ .

No exchange property is assumed. The lemma transfers maximization questions about $g$ on the lattice points to the concave function $\hat g$ on the polytope $\overline B$ .

Formalization Note. Part (2) is stated as: some $b\in\overline B$ has $\hat g(b)=\max_B g$ , and $\hat g(b)\le\max_B g$ for all $b\in\overline B$ . All three parts evaluate $\hat g$ only on $\overline B$ (see the definition of concaveClosure).

Preamble

import Mathlib
import Definitions.Def_SteinitzExchange_Extension_IntegralBaseSet
import Definitions.Def_SteinitzExchange_Extension_Exchange
import Definitions.Def_SteinitzExchange_Extension_ConcaveClosure

Formal statement

namespace SteinitzExchange.Extension

/-- Murota 1996, p. 285, Lemma 4.1, for any `g : B → ℝ` on a nonempty finite `B ⊆ ℤ^V`:
(1) `ĝ(x) ≥ g(x)` for `x ∈ B`;
(2) `max{ĝ(b) | b ∈ B̄} = max{g(x) | x ∈ B}` (the left maximum is attained);
(3) `argmax(ĝ) = conv(argmax(g))`, the argmax of `ĝ` taken over `B̄`. -/
theorem concaveClosure_basic {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (B : Finset (V → ℤ)) (hB : B.Nonempty) (g : (V → ℤ) → ℝ) :
    (∀ x ∈ B, g x ≤ concaveClosure B g (toReal x)) ∧
    ((∃ b ∈ hull B, concaveClosure B g b = B.sup' hB g) ∧
      ∀ b ∈ hull B, concaveClosure B g b ≤ B.sup' hB g) ∧
    argmaxOn (hull B) (concaveClosure B g) = hull (argmaxB B g) := by sorry

end SteinitzExchange.Extension

Source

Murota, Convexity and Steinitz's Exchange Property, Adv. Math. 124 (1996), p. 285, Lemma 4.1

Read-back

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

Setting. $V$ is a finite, nonempty type with decidable equality. The symbols used are:

$\iota(x)$ is $x \in \mathbb{Z}^V$ read in $\mathbb{R}^V$ .
$\langle p, b\rangle = \sum_v p(v) b(v)$ .
$B \subseteq \mathbb{Z}^V$ is a nonempty finite set. It is not assumed to be an integral base set.
$g : \mathbb{Z}^V \to \mathbb{R}$ is arbitrary.

Definitions used.

$\bar B$ is the real convex hull of $\{\iota(x) : x\in B\}$ .
The conjugate is

g^\circ(p) = \min_{x\in B}\big(\langle p, \iota(x)\rangle - g(x)\big).

The closure is

\hat g(b) = \inf_{p\in\mathbb{R}^V}\big(\langle p,b\rangle - g^\circ(p)\big),

taken as a real infimum. It takes the value $0$ when the family is not bounded below.

$\operatorname{argmax}_B(g) = \{x\in B : g(y)\le g(x)\ \forall y\in B\}$ .
$\operatorname{argmax}_{\bar B}(\hat g) = \{b\in\bar B : \hat g(c)\le\hat g(b)\ \forall c\in\bar B\}$ .

Let $M = \max_{x \in B} g(x)$ .

Conclusion. Three claims hold together:

$g(x) \le \hat g(\iota(x))$ for every $x \in B$ .
There is some $b \in \bar B$ with $\hat g(b) = M$ , and $\hat g(b) \le M$ for every $b \in \bar B$ .
$\operatorname{argmax}_{\bar B}(\hat g)$ equals the convex hull of $\{\iota(x) : x \in \operatorname{argmax}_B(g)\}$ .

Degenerate cases.

If $B = \{x\}$ $B = {x}$ , then $\bar B = \{\iota(x)\}$ $\overset{ˉ}{B} = {ι (x)}$ . The claims say:
- $g(x) \le \hat g(\iota(x))$ and $\hat g(\iota(x)) = g(x)$ ;
- both argmax sets equal $\{\iota(x)\}$ .
$\hat g$ is only evaluated at points of $\bar B$ , so its behaviour outside $\bar B$ is not constrained here.
If $\hat g(b)$ took the default value $0$ for some $b \in \bar B$ , claims 2 and 3 would apply to that default value.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 4.1 — the concave closure dominates ggg on BBB, has the same maximum, and its maximizers are argmax⁡(g)‾\overline{\operatorname{argmax}(g)}argmax(g)​

Lemma 4.1 — the concave closure dominates $g$ on $B$ , has the same maximum, and its maximizers are $\overline{\operatorname{argmax}(g)}$