DemandSet

Definition

DiscreteConvex_EconomicEquilibriumB_DemandSet

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

discrete-convex-analysis

The demand set $D_h(p)=\arg\max(U_h(x)-\langle p,x\rangle)$ .

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

Definition code

import Mathlib
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_ArgMaxBot
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_PriceShift

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The demand set `Dh(p) = arg max (Uh(x) − ⟨p,x⟩)`. -/
def DemandSet (U : (K → ℤ) → WithBot ℝ) (p : K → ℝ) : Set (K → ℤ) := ArgMaxBot (PriceShift U p)

end DiscreteConvex.EconomicEquilibriumB

Source

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

View graph