IsConcaveExtensible

Definition

DiscreteConvex_EconomicEquilibriumB_IsConcaveExtensible

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

convex-optimizationdiscrete-convex-analysis

$U$ is concave-extensible: it agrees with its own concave closure on its domain.

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

Definition code

import Mathlib
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_UDom
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_ToERealOfBot
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_ConcaveClosureR

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- `U` is concave-extensible: it agrees with its own concave closure on its domain. -/
def IsConcaveExtensible (U : (K → ℤ) → WithBot ℝ) : Prop :=
  ∀ x : K → ℤ, x ∈ UDom U → ConcaveClosureR U (fun v => (x v : ℝ)) = ToERealOfBot (U x)

end DiscreteConvex.EconomicEquilibriumB

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.331, redeclared property

View graph