Theorem 6.39 -- mconvex_minimizer_cut_scaling

Proved

DiscreteConvex.MConvexFunctionsC.mconvex_minimizer_cut_scaling

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

convex-optimizationdiscrete-convex-analysis

Theorem 6.39 (M-minimizer cut with scaling; p.158). Let $f$ be M-convex with $\arg\min f \ne \emptyset$ , $\alpha$ a positive integer, $n=|V|$ . (1) For $x\in\operatorname{dom} f$ , $v\in V$ , and $u$ minimizing $f(x+\alpha(\chi_v-\chi_u))$ over shifts at $v$ , some minimizer $x^*$ of $f$ has $x^*(u) \le x(u) - \alpha(1-\chi_v(u)) + (n-1)(\alpha-1)$ . (2) The symmetric statement for the lower bound at $v$ .

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

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_MConvexFunctionsC_CharVec
import Definitions.Def_DiscreteConvex_MConvexFunctionsC_DomZ
import Definitions.Def_DiscreteConvex_MConvexFunctionsC_MExchangeAxiom
import Definitions.Def_DiscreteConvex_MConvexFunctionsC_ArgMinOn

Formal statement

namespace DiscreteConvex.MConvexFunctionsC

open scoped Pointwise
open Classical
variable {V : Type*} [Fintype V] [DecidableEq V]
/-- Theorem 6.39 (p.158), M-minimizer cut with scaling. -/
theorem mconvex_minimizer_cut_scaling (f : (V → ℤ) → WithTop ℝ) (hf : MExchangeAxiom f)
    (hne : (ArgMinOn f).Nonempty) (alpha : ℤ) (halpha : 0 < alpha) :
    (∀ x ∈ DomZ f, ∀ v u : V,
        (∀ s : V, f (fun w => x w + alpha * (CharVec v w - CharVec u w)) ≤
          f (fun w => x w + alpha * (CharVec v w - CharVec s w))) →
        ∃ xstar ∈ ArgMinOn f,
          xstar u ≤ x u - alpha * (1 - CharVec v u) + ((Fintype.card V : ℤ) - 1) * (alpha - 1)) ∧
    (∀ x ∈ DomZ f, ∀ u v : V,
        (∀ t : V, f (fun w => x w + alpha * (CharVec v w - CharVec u w)) ≤
          f (fun w => x w + alpha * (CharVec t w - CharVec u w))) →
        ∃ xstar ∈ ArgMinOn f,
          xstar v ≥ x v + alpha * (1 - CharVec u v) - ((Fintype.card V : ℤ) - 1) * (alpha - 1)) := by sorry

end DiscreteConvex.MConvexFunctionsC

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.158, Theorem 6.39

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