Lemma 6.3 — weak duality and the Fenchel identity (6.5) for arbitrary functions on finite sets

Proved

SteinitzExchange.Duality.weak_duality

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

discrete-convex-analysisfenchel-dualityp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1weak-duality

Let $B_1,B_2\subseteq\mathbb Z^V$ be finite nonempty sets (no exchange axiom is assumed), and let $\omega:B_1\to\mathbb R$ , $\zeta:B_2\to\mathbb R$ be arbitrary. With the conjugates $\omega^\circ,\zeta^\bullet$ and the closures $\hat\omega,\check\zeta$ taken with respect to $B_1$ and $B_2$ respectively,

\max\{\omega(x)-\zeta(x)\mid x\in B_1\cap B_2\}\;\le\;\max\{\hat\omega(b)-\check\zeta(b)\mid b\in\overline{B_1}\cap\overline{B_2}\}\;=\;\inf\{\zeta^\bullet(p)-\omega^\circ(p)\mid p\in\mathbb R^V\},

where a maximum over an empty family is $-\infty$ and the infimum may be $-\infty$ . When $\overline{B_1}\cap\overline{B_2}\neq\emptyset$ , the middle maximum is attained.

The equality is the Fenchel duality (6.5) for the polyhedral concave function $\hat\omega$ and polyhedral convex function $\check\zeta$ ; it holds with no constraint qualification. The inequality is the weak half of the min-max theorem of the mission.

Formalization Note. All three values are in EReal (primalValue, relaxedValue, dualValue). "Max" is rendered as a supremum together with an explicit attainment clause for the relaxed problem; the primal maximum is over a finite set.

Preamble

import Mathlib
import Definitions.Def_SteinitzExchange_Duality_IntegralBaseSet
import Definitions.Def_SteinitzExchange_Duality_Conjugate
import Definitions.Def_SteinitzExchange_Duality_Problems

Formal statement

namespace SteinitzExchange.Duality

/-- Murota 1996, p. 295, Lemma 6.3 (weak duality, with the Fenchel identity (6.5)): for any
functions `ω : B₁ → ℝ` and `ζ : B₂ → ℝ` on nonempty finite sets `B₁, B₂ ⊆ ℤ^V` (no (B1) needed),
`max{ω(x) − ζ(x) | x ∈ B₁ ∩ B₂} ≤ max{ω̂(b) − ζ̌(b) | b ∈ B̄₁ ∩ B̄₂}
  = inf{ζ•(p) − ω°(p) | p ∈ ℝ^V}`,
all values in `EReal` with `max ∅ = −∞`; the relaxed maximum is attained when `B̄₁ ∩ B̄₂ ≠ ∅`. -/
theorem weak_duality {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (B₁ B₂ : Finset (V → ℤ)) (hB₁ : B₁.Nonempty) (hB₂ : B₂.Nonempty)
    (ω ζ : (V → ℤ) → ℝ) :
    primalValue B₁ B₂ ω ζ ≤ relaxedValue B₁ B₂ ω ζ ∧
    relaxedValue B₁ B₂ ω ζ = dualValue B₁ B₂ ω ζ ∧
    ((hull B₁ ∩ hull B₂).Nonempty →
      ∃ b ∈ hull B₁ ∩ hull B₂,
        relaxedValue B₁ B₂ ω ζ = ((concaveClosure B₁ ω b - convexClosure B₂ ζ b : ℝ) : EReal)) := by sorry

end SteinitzExchange.Duality

Source

Murota, Convexity and Steinitz's Exchange Property, Adv. Math. 124 (1996), p. 295, Lemma 6.3 (and Eq. (6.5), pp. 294-295)

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.
$B_1, B_2 \subseteq \mathbb{Z}^V$ are nonempty finite sets. They are not assumed to be integral base sets.
$\omega, \zeta : \mathbb{Z}^V \to \mathbb{R}$ are arbitrary.

The notation is as follows, with all values in the extended reals:

$\mathrm{P} = \sup\{\omega(x) - \zeta(x) : x \in B_1\cap B_2\}$ , where the empty supremum is $-\infty$ .
$\mathrm{R} = \sup\{\hat\omega(b) - \check\zeta(b) : b \in \overline{B_1}\cap\overline{B_2}\}$ . Here $\overline{B_i}$ is the real convex hull of $B_i$ . The closures are real-valued: $\hat\omega(b) = \inf_{p\in\mathbb{R}^V}(\langle p,b\rangle - \omega^\circ(p))$ and $\check\zeta(b) = \sup_{p}(\langle p,b\rangle - \zeta^\bullet(p))$ .
$\mathrm{D} = \inf_{p \in \mathbb{R}^V}\bigl(\zeta^\bullet(p) - \omega^\circ(p)\bigr)$ .
The conjugates are $\omega^\circ(p) = \min_{x\in B_1}(\langle p,x\rangle - \omega(x))$ and $\zeta^\bullet(p) = \max_{x \in B_2}(\langle p,x\rangle - \zeta(x))$ , where $\langle p, x\rangle = \sum_v p(v)x(v)$ .

Claim. The theorem asserts all three of the following:

$\mathrm{P} \le \mathrm{R}$ .
$\mathrm{R} = \mathrm{D}$ .
If $\overline{B_1} \cap \overline{B_2} \neq \emptyset$ , then some $b \in \overline{B_1}\cap\overline{B_2}$ attains the relaxed value:

\mathrm{R} = \hat\omega(b) - \check\zeta(b).

Degenerate cases. If $B_1 \cap B_2 = \emptyset$ , then $\mathrm{P} = -\infty$ and part 1 is automatic. If $\overline{B_1}\cap\overline{B_2} = \emptyset$ , then $\mathrm{R} = -\infty$ , part 3 is vacuous, and part 2 asserts $\mathrm{D} = -\infty$ , i.e. that $\zeta^\bullet - \omega^\circ$ is unbounded below on $\mathbb{R}^V$ . Because $B_1, B_2$ are nonempty, the conjugates are genuine minima and maxima. The closures are evaluated only at points of the hulls, so the junk value $0$ used for points outside a hull never enters. Empty $V$ is excluded by hypothesis.

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