The law of diminishing marginal utility

Proved

MarginalUtility.law_of_diminishing_marginal_utility

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

concavityeconomicsmarginal-utilitymicroeconomics

Throughout, a utility function of one quantified variable is a map $U:\mathbb R\to\mathbb R$ (all other variables held fixed, ceteris paribus); $\Delta U(s_1\to s_2)=U(s_2)-U(s_1)$ is the change in utility from state $s_1$ to state $s_2$ ; the marginal utility at $g$ is $\partial U/\partial g=U'(g)$ ; and $U$ has diminishing marginal utility on a set $D\subseteq\mathbb R$ when $U$ and $U'$ are differentiable on $D$ and $\partial^2U/\partial g^2<0$ at every point of $D$ . An open interval $D$ below means an open convex subset of $\mathbb R$ (possibly empty, possibly unbounded).

Let $D\subseteq\mathbb R$ be an open interval and let $U$ have diminishing marginal utility on $D$ , i.e. $\partial^2U/\partial g^2<0$ on $D$ . Then (i) as the amount consumed increases, marginal utility goes on decreasing: $U'$ is strictly decreasing on $D$ ; and (ii) each additional gain produces a smaller increase in utility than the previous gain of equal size: for every $h>0$ and $x$ with $x,\,x+2h\in D$ ,

U(x+2h)-U(x+h)<U(x+h)-U(x).

Preamble

import Mathlib
import Definitions.Def_MarginalUtility_Model

open Filter Topology Set

Formal statement

namespace MarginalUtility

theorem law_of_diminishing_marginal_utility (U : ℝ → ℝ) (D : Set ℝ)
    (hDo : IsOpen D) (hDc : Convex ℝ D) (hU : HasDiminishingMarginalUtility U D) :
    StrictAntiOn (marginalUtility U) D ∧
      ∀ x h : ℝ, 0 < h → x ∈ D → x + 2 * h ∈ D →
        utilityChange U (x + h) (x + 2 * h) < utilityChange U x (x + h) := by sorry

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.

Let $U:\mathbb R\to\mathbb R$ and let $D\subseteq\mathbb R$ be open and convex (an open interval, possibly empty or unbounded). Assume $U$ has diminishing marginal utility on $D$ : $U$ is differentiable on $D$ , the derivative function $U'$ is differentiable on $D$ , and $(U')'(g)<0$ for every $g\in D$ . The conclusion is the conjunction of:

$g\mapsto\mathrm{MU}_U(g)=U'(g)$ is strictly decreasing on $D$ : for $a<b$ in $D$ , $U'(b)<U'(a)$ ;
for all real $x,h$ with $h>0$ , $x\in D$ and $x+2h\in D$ ,

U(x+2h)-U(x+h)<U(x+h)-U(x),

where both sides are the defined utility changes $\Delta U(x+h,x+2h)$ and $\Delta U(x,x+h)$ .

If $D$ is empty, both parts hold trivially.

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