Theorem 11.5 -- gs_iff_mnatural_concave

Open

DiscreteConvex.EconomicEquilibriumB.gs_iff_mnatural_concave

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

convex-optimizationdiscrete-convex-analysis

Theorem 11.5 (p.331). For a concave-extensible function $U:\mathbb Z^K\to\mathbb R\cup\{-\infty\}$ with a bounded nonempty effective domain, $U$ is M $^ atural$ -concave iff $U$ satisfies (−M $^ atural$ -GS[Z]).

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

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_UDom
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_MNaturalConcave
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_IsConcaveExtensible
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_NegGS

Formal statement

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- Theorem 11.5 (p.331). For a concave-extensible function `U` with bounded nonempty effective
domain, `U` is M♮-concave iff `U` satisfies (−M♮-GS[Z]). -/
theorem gs_iff_mnatural_concave (U : (K → ℤ) → WithBot ℝ) (hconc : IsConcaveExtensible U)
    (hbdd : ∃ N : ℤ, ∀ x ∈ UDom U, ∀ k, |x k| ≤ N) (hne : (UDom U).Nonempty) :
    MNaturalConcave U ↔ NegGS U := by sorry

end DiscreteConvex.EconomicEquilibriumB

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.331, Theorem 11.5

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