Prove2Me

Eq. (5.12) — the localization of ω° at p₀ is the minimum of ⟨p, x⟩ over argmax(ω[−p₀])

Proved
SteinitzExchange.LocalSupermod.localization_eq_min_argmax

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

concave-conjugatem-concavep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1subdifferential

Let B⊆ZVB\subseteq\mathbb Z^V be a finite integral base set, ω:B→R\omega:B\to\mathbb R, and p0,p∈RVp_0,p\in\mathbb R^V. The localization of the concave conjugate ω∘\omega^\circ at p0p_0, defined through the subdifferential ∂ω∘(p0)\partial\omega^\circ(p_0), satisfies

L^(ω∘,p0)(p)=min⁡{⟨p,x⟩∣x∈argmax⁡(ω[−p0])},\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\},

the minimum being attained.

This identity reduces the localization of ω∘\omega^\circ to the support function ψ∘\psi^\circ of the maximizer set argmax⁡(ω[−p0])\operatorname{argmax}(\omega[-p_0]), which is the bridge between the Local Supermodularity Theorem and Theorems 4.4 and 5.1.

Formalization Note. The identity is stated as IsLeast: L^(ω∘,p0)(p)\hat L(\omega^\circ,p_0)(p) is a value ⟨p,x⟩\langle p,x\rangle at some maximizer xx and is at most every such value. This excludes the junk value of the real sInf in the definition of the localization. Note the sign: ω[−p0](x)=ω(x)−⟨p0,x⟩\omega[-p_0](x)=\omega(x)-\langle p_0,x\rangle.

Preamble
import Mathlib
import Definitions.Def_SteinitzExchange_LocalSupermod_IntegralBaseSet
import Definitions.Def_SteinitzExchange_LocalSupermod_Exchange
import Definitions.Def_SteinitzExchange_LocalSupermod_Localization
Formal statement
namespace SteinitzExchange.LocalSupermod

/-- Murota 1996, p. 292, Eq. (5.12). For `ω` on a finite integral base set `B`, every `p₀`
and every `p`, the localization `L̂(ω°, p₀)(p)` (defined by (5.8)–(5.9)) is the minimum of
`⟨p, x⟩` over `x ∈ argmax(ω[−p₀])`: it is attained there and is a lower bound. -/
theorem localization_eq_min_argmax {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (B : Finset (V → ℤ)) (hB : IsIntegralBaseSet B) (ω : (V → ℤ) → ℝ) (p₀ p : V → ℝ) :
    IsLeast ((fun x => pairing p (toReal x)) '' (argmaxB B (perturb ω (-p₀)) : Set (V → ℤ)))
      (localization (concaveConj B ω) p₀ p) := by sorry

end SteinitzExchange.LocalSupermod
Source
Murota, Convexity and Steinitz's Exchange Property, Adv. Math. 124 (1996), p. 292, Eq. (5.12) (proof of Theorem 5.3)
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, and ⟨p,b⟩=∑vp(v) b(v)\langle p, b\rangle = \sum_v p(v)\,b(v).
  • B⊆ZVB \subseteq \mathbb{Z}^V is a finite integral base set. That means B≠∅B \neq \emptyset, 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.
  • ω:ZV→R\omega : \mathbb{Z}^V \to \mathbb{R} is arbitrary, and p0,p∈RVp_0, p \in \mathbb{R}^V are arbitrary.

Definitions used.

  • The concave conjugate is
ω∘(q)=min⁡x∈B(⟨q,x⟩−ω(x)).\omega^\circ(q) = \min_{x \in B} \big(\langle q, x\rangle - \omega(x)\big).
  • Its superdifferential at p0p_0 is
∂ω∘(p0)={b∈RV:ω∘(q)−ω∘(p0)≤⟨q−p0,b⟩ ∀q∈RV}.\partial\omega^\circ(p_0) = \{b \in \mathbb{R}^V : \omega^\circ(q) - \omega^\circ(p_0) \le \langle q - p_0, b\rangle \ \forall q \in \mathbb{R}^V\}.
  • The localization is
L^(ω∘,p0)(p)=inf⁡{⟨p,b⟩:b∈∂ω∘(p0)},\hat L(\omega^\circ, p_0)(p) = \inf\{\langle p, b\rangle : b \in \partial\omega^\circ(p_0)\},

taken as a real infimum. It takes the default value 00 if that set is empty or unbounded below.

Claim. Let

A={x∈B:ω(x)−⟨p0,x⟩≥ω(y)−⟨p0,y⟩ ∀y∈B}.A = \{x \in B : \omega(x) - \langle p_0, x\rangle \ge \omega(y) - \langle p_0, y\rangle \ \forall y \in B\}.

Then L^(ω∘,p0)(p)\hat L(\omega^\circ, p_0)(p) is the least element of {⟨p,x⟩:x∈A}\{\langle p, x\rangle : x \in A\}. In other words, it is attained as ⟨p,x⟩\langle p, x\rangle for some x∈Ax \in A, and it is ≤⟨p,x⟩\le \langle p, x\rangle for every x∈Ax \in A.

Degenerate cases.

  • Empty VV and empty BB are excluded. The set AA is nonempty because BB is finite and nonempty.
  • If B={x0}B = \{x_0\} has one element, then A={x0}A = \{x_0\}, and the theorem asserts L^(ω∘,p0)(p)=⟨p,x0⟩\hat L(\omega^\circ, p_0)(p) = \langle p, x_0\rangle.
  • p=0p = 0 is allowed. The claim then gives the value 00.
  • The theorem fixes the left-hand value as the stated real infimum under the default-value convention. It asserts that this value equals the minimum over AA.
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