PriceShift

Definition

DiscreteConvex_EconomicEquilibriumB_PriceShift

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

convex-optimizationdiscrete-convex-analysis

The price-shifted utility $U[-p](x)=U(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

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The price-shifted utility `U[−p](x) = U(x) − ⟨p,x⟩`. -/
def PriceShift (U : (K → ℤ) → WithBot ℝ) (p : K → ℝ) (x : K → ℤ) : WithBot ℝ :=
  U x + ((-(∑ k, p k * (x k : ℝ)) : ℝ) : WithBot ℝ)

end DiscreteConvex.EconomicEquilibriumB

Source

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

View graph