SupplySet

Definition

DiscreteConvex_EconomicEquilibriumB_SupplySet

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

discrete-convex-analysis

The supply set $S_l(p)=\arg\min C_l[-p]$ .

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.324, Eq. (11.1), redeclared.)

Definition code

import Mathlib
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_ArgMinTop
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_PriceShiftConvex

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The supply set `Sl(p) = arg min Cl[−p]`. -/
def SupplySet (C : (K → ℤ) → WithTop ℝ) (p : K → ℝ) : Set (K → ℤ) :=
  ArgMinTop (PriceShiftConvex C p)

end DiscreteConvex.EconomicEquilibriumB

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.324, Eq. (11.1), redeclared

View graph