Theorem 8.32 -- m2_optimality_criterion

Proved

DiscreteConvex.ConjugacyDualityB.m2_optimality_criterion

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

combinatoricsdiscrete-convex-analysis

Theorem 8.32 (M2-optimality criterion; p.227). For an M2-convex function $f$ and $x\in\operatorname{dom} f$ : $x$ globally minimizes $f$ iff $f(x)\le f(x+\chi_Y-\chi_Z)$ for all $Y,Z\subseteq V$ with $|Y|=|Z|$ .

Not in this chunk's own BRIEF.md table — found by direct reading, immediately following Theorem 8.31 on the same page (PDF245), the chunk's own last assigned page.

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.227, Theorem 8.32.)

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_ConjugacyDualityB_IndicatorVec
import Definitions.Def_DiscreteConvex_ConjugacyDualityB_DomZ
import Definitions.Def_DiscreteConvex_ConjugacyDualityB_M2Convex

Formal statement

namespace DiscreteConvex.ConjugacyDualityB

open Classical
open scoped Pointwise
variable {V : Type*} [Fintype V] [DecidableEq V]
/-- Theorem 8.32 (M2-optimality criterion; p.227). Global optimality of an M2-convex function is
characterized by non-improvement under equal-size coordinate swaps. -/
theorem m2_optimality_criterion (f : (V → ℤ) → WithTop ℝ) (hf : M2Convex f) (x : V → ℤ)
    (hx : x ∈ DomZ f) :
    (∀ y : V → ℤ, f x ≤ f y) ↔
      (∀ Y Z : Finset V, Y.card = Z.card →
        f x ≤ f (fun v => x v + IndicatorVec Y v - IndicatorVec Z v)) := by sorry

end DiscreteConvex.ConjugacyDualityB

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.227, Theorem 8.32

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