Prove2Me

Lemma 4.5 — an M-concave function coincides with its concave closure on BB

Proved
SteinitzExchange.Duality.concaveClosure_eq_of_exc

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

concave-closureexchange-propertym-concavep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let B⊆ZVB\subseteq\mathbb Z^V be a finite integral base set and let ω:B→R\omega:B\to\mathbb R satisfy the exchange property (EXC). Then

ω^(x)=ω(x)for all x∈B,\hat\omega(x)=\omega(x)\qquad\text{for all }x\in B,

where ω^\hat\omega is the concave closure of ω\omega.

For arbitrary ω\omega only ω^≥ω\hat\omega\ge\omega holds on BB; (EXC) makes the concave closure an extension of ω\omega. In the duality theorem this is what makes an integral optimum of the relaxed primal problem an optimum of the primal problem.

Preamble
import Mathlib
import Definitions.Def_SteinitzExchange_Duality_IntegralBaseSet
import Definitions.Def_SteinitzExchange_Duality_Exchange
import Definitions.Def_SteinitzExchange_Duality_Conjugate
Formal statement
namespace SteinitzExchange.Duality

/-- Murota 1996, p. 288, Lemma 4.5: if `ω` satisfies (EXC) on the finite integral base set `B`,
then its concave closure agrees with it on `B`: `ω̂(x) = ω(x)` for all `x ∈ B`. -/
theorem concaveClosure_eq_of_exc {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (B : Finset (V → ℤ)) (hB : IsIntegralBaseSet B) (ω : (V → ℤ) → ℝ)
    (hω : SatisfiesEXC B ω) :
    ∀ x ∈ B, concaveClosure B ω (toReal x) = ω x := by sorry

end SteinitzExchange.Duality
Source
Murota, Convexity and Steinitz's Exchange Property, Adv. Math. 124 (1996), p. 288, Lemma 4.5
Read-back

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

Setting.

  • VV is a finite, nonempty type with decidable equality.
  • B⊆ZVB \subseteq \mathbb{Z}^V is an integral base set: nonempty, and for all x,y∈Bx, y \in B and every uu with (x−y)(u)>0(x-y)(u) > 0 there is vv with (x−y)(v)<0(x-y)(v) < 0 and x−χu+χv∈Bx - \chi_u + \chi_v \in B. Here χu\chi_u is the unit integer vector at uu.
  • ω:ZV→R\omega : \mathbb{Z}^V \to \mathbb{R} satisfies (EXC) on BB: for all x,y∈Bx, y \in B and every uu with (x−y)(u)>0(x-y)(u) > 0, there is vv with (x−y)(v)<0(x-y)(v) < 0 such that
    • x−χu+χv∈Bx - \chi_u + \chi_v \in B and y+χu−χv∈By + \chi_u - \chi_v \in B;
    • ω(x)+ω(y)≤ω(x−χu+χv)+ω(y+χu−χv)\omega(x)+\omega(y) \le \omega(x-\chi_u+\chi_v) + \omega(y+\chi_u-\chi_v).

Claim. For every x∈Bx \in B:

ω^(x)=ω(x).\hat\omega(x) = \omega(x).

Here ω^\hat\omega is the concave closure with respect to BB, evaluated at xx viewed as a real vector:

ω^(b)=inf⁡p∈RV(⟨p,b⟩−ω∘(p)),ω∘(p)=min⁡y∈B(⟨p,y⟩−ω(y)).\hat\omega(b) = \inf_{p\in\mathbb{R}^V}\bigl(\langle p,b\rangle - \omega^\circ(p)\bigr), \qquad \omega^\circ(p) = \min_{y \in B}\bigl(\langle p,y\rangle - \omega(y)\bigr).

The first infimum is a real infimum (junk value 00 if unbounded).

Degenerate cases. If BB has a single element, both hypotheses hold vacuously for every ω\omega. The claim then says that the concave closure at that point equals ω\omega there. Empty VV and empty BB are excluded.

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