Theorem 11.6 -- swgs_iff_mnatural_concave

Open

DiscreteConvex.EconomicEquilibriumB.swgs_iff_mnatural_concave

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

convex-optimizationdiscrete-convex-analysis

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

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

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_NegSWGS

Formal statement

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- Theorem 11.6 (p.331). For a concave-extensible function `U` with nonempty effective domain,
`U` is M♮-concave iff `U` satisfies (−M♮-SWGS[Z]). -/
theorem swgs_iff_mnatural_concave (U : (K → ℤ) → WithBot ℝ) (hconc : IsConcaveExtensible U)
    (hne : (UDom U).Nonempty) :
    MNaturalConcave U ↔ NegSWGS U := by sorry

end DiscreteConvex.EconomicEquilibriumB

Source

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

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