Utility change $\Delta U$ , marginal utility $\partial U/\partial g$ , diminishing marginal utility $\partial^2 U/\partial g^2<0$

Definition

MarginalUtility_Model

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

concavityeconomicsmarginal-utilitymicroeconomics

This file fixes the vocabulary of the section Quantified marginal utility.

Change in utility. For any set of states $S$ , a utility $U:S\to\mathbb R$ and states $s_1,s_2\in S$ ,

\Delta U(s_1\to s_2)=U(s_2)-U(s_1).

Marginal utility. For a utility $U:\mathbb R\to\mathbb R$ of a single quantified variable $g$ (everything else held fixed, c.p.),

\frac{\partial U}{\partial g}(g)=U'(g),

the derivative of $U$ at $g$ . (Lean's deriv returns $0$ where $U$ is not differentiable; every statement in this mission that uses marginal utility also assumes the differentiability it needs.) 3. Diminishing marginal utility on $D\subseteq\mathbb R$ . $U$ is differentiable on $D$ , its marginal utility $U'$ is differentiable on $D$ , and

\frac{\partial^2 U}{\partial g^2}(g)<0\quad\text{for every } g\in D.

Definition code

import Mathlib

namespace MarginalUtility

/-- Change in utility when moving from state `s₁` to state `s₂`:
`ΔU = U(s₂) - U(s₁)`. -/
def utilityChange {S : Type*} (U : S → ℝ) (s₁ s₂ : S) : ℝ :=
  U s₂ - U s₁

/-- Marginal utility `∂U/∂g` of a utility function `U` of a single quantified variable `g`
(all other variables held fixed, *ceteris paribus*): the derivative of `U` at `g`. -/
noncomputable def marginalUtility (U : ℝ → ℝ) (g : ℝ) : ℝ :=
  deriv U g

/-- `U` has diminishing marginal utility on the set `D`: `U` is differentiable on `D`, its
marginal utility `∂U/∂g` is differentiable on `D`, and `∂²U/∂g² < 0` at every point of `D`. -/
def HasDiminishingMarginalUtility (U : ℝ → ℝ) (D : Set ℝ) : Prop :=
  DifferentiableOn ℝ U D ∧ DifferentiableOn ℝ (deriv U) D ∧
    ∀ g ∈ D, deriv (deriv U) g < 0

end MarginalUtility

Source

Wikipedia, "Marginal utility" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Marginal_utility

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It is not independent, blind testimony and must not be mistaken for one. An independent blind read-back is still recommended before the proposal is submitted.

The file declares three objects.

Utility change. For an arbitrary type $S$ , a real-valued function $U:S\to\mathbb R$ and two elements $s_1,s_2\in S$ , the quantity $\Delta U(s_1,s_2)$ is defined as the real number $U(s_2)-U(s_1)$ (second argument minus first). No hypothesis is placed on $S$ or $U$ .

Marginal utility. For a function $U:\mathbb R\to\mathbb R$ and a point $g\in\mathbb R$ , $\mathrm{MU}_U(g)$ is defined as the derivative of $U$ at $g$ . Edge case: if $U$ is not differentiable at $g$ , this value is by convention $0$ (it is not undefined), so $\mathrm{MU}_U(g)=0$ alone does not imply differentiability.

Diminishing marginal utility on $D$ . For $U:\mathbb R\to\mathbb R$ and an arbitrary subset $D\subseteq\mathbb R$ , the predicate holds exactly when all three of the following hold: (i) $U$ is differentiable on $D$ (in the within- $D$ sense); (ii) the global derivative function $g\mapsto U'(g)$ (with the value- $0$ convention above) is differentiable on $D$ (within $D$ ); (iii) for every $g\in D$ , the derivative at $g$ of the global function $U'$ is strictly negative:

(U')'(g)<0\qquad (g\in D).

Condition (iii) uses the ordinary (two-sided) derivative of $U'$ at $g$ , not a derivative within $D$ ; when $D$ is not open these can differ. If $D$ is empty the predicate holds for every $U$ . No openness, convexity or nonemptiness of $D$ is required by the definition itself.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Utility change ΔU\Delta UΔU, marginal utility ∂U/∂g\partial U/\partial g∂U/∂g, diminishing marginal utility ∂2U/∂g2<0\partial^2 U/\partial g^2<0∂2U/∂g2<0

Utility change $\Delta U$ , marginal utility $\partial U/\partial g$ , diminishing marginal utility $\partial^2 U/\partial g^2<0$