Proposition 3.19 -- integral convexity is pointwise-local

Proved

DiscreteConvex.IntegralConvexity.integrally_convex_iff_restriction

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

convex-optimizationdiscrete-convex-analysis

Proposition 3.19 (p.94). A function $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ is integrally convex if and only if its restriction $f_{[a,b]}$ to every integer interval $[a,b]$ is integrally convex.

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

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_IntegralConvexity_IntegrallyConvex
import Definitions.Def_DiscreteConvex_IntegralConvexity_Restrict

Formal statement

namespace DiscreteConvex.IntegralConvexity

/-- Proposition 3.19 (Murota, *Discrete Convex Analysis*, SIAM 2003, p.94). A function
`f : Zⁿ → R ∪ {+∞}` is integrally convex if and only if its restriction `f_{[a,b]}` to every
integer interval `[a,b]` is integrally convex. -/
theorem integrally_convex_iff_restriction {n : ℕ} (f : (Fin n → ℤ) → WithTop ℝ) :
    IntegrallyConvex f ↔ ∀ a b : Fin n → ℤ, IntegrallyConvex (Restrict f a b) := by sorry

end DiscreteConvex.IntegralConvexity

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.94, Proposition 3.19

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