Proposition 3.18 -- convex extensibility and hole-free perturbed minimizers

Proved

DiscreteConvex.IntegralConvexity.convex_extensible_iff_argmin_hole_free

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

convex-optimizationdiscrete-convex-analysisdiscrete-geometry

Proposition 3.18 (p.93). If $f$ is convex extensible, then $\arg\min f[-p]$ is hole free for every $p \in \mathbb R^n$ . The converse also holds if $\operatorname{dom}_{\mathbb Z} f$ is bounded.

Formalization Note. Boundedness of $\operatorname{dom}_{\mathbb Z} f$ is represented as the existence of a single real bound $R$ on every coordinate of every point of the domain, the natural reading of "bounded" for a subset of $\mathbb Z^n$ .

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.93, Proposition 3.18.)

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_IntegralConvexity_ConvexExtensible
import Definitions.Def_DiscreteConvex_IntegralConvexity_ArgMinPerturbed
import Definitions.Def_DiscreteConvex_IntegralConvexity_HoleFree

Formal statement

namespace DiscreteConvex.IntegralConvexity

/-- Proposition 3.18 (Murota, *Discrete Convex Analysis*, SIAM 2003, p.93). If `f` is convex
extensible, then `arg min f[-p]` is hole free for every `p ∈ Rⁿ`. The converse also holds if
`dom_Z f` is bounded (represented here as a common real bound on the coordinates of every
point of the domain). -/
theorem convex_extensible_iff_argmin_hole_free {n : ℕ} (f : (Fin n → ℤ) → WithTop ℝ) :
    (ConvexExtensible f → ∀ p : Fin n → ℝ, HoleFree (ArgMinPerturbed f p)) ∧
    ((∃ R : ℝ, ∀ x : Fin n → ℤ, f x ≠ ⊤ → ∀ i, |(x i : ℝ)| ≤ R) →
      (∀ p : Fin n → ℝ, HoleFree (ArgMinPerturbed f p)) → ConvexExtensible f) := by sorry

end DiscreteConvex.IntegralConvexity

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.93, Proposition 3.18

Human review

Endorsed by Community (Bot) · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph