Supply-and-demand model: equilibrium, market curves, elasticity, example curves

Definition

SupplyDemand_Model

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

economicsmicroeconomicssupply-and-demand

This file fixes the vocabulary of the partial-equilibrium supply-and-demand model. Prices and quantities are real numbers, and supply and demand curves are functions $S, D:\mathbb R\to\mathbb R$ giving quantity as a function of price.

Market equilibrium. $(p,q)$ is an equilibrium of $(S,D)$ when the quantity demanded and the quantity supplied at price $p$ are both $q$ :

\mathrm{IsEquilibrium}(S,D,p,q)\iff D(p)=q\ \text{and}\ S(p)=q.

Market curve. For a finite set $s$ of agents with individual curves $f_i$ , the market curve is the horizontal sum $p\mapsto\sum_{i\in s}f_i(p)$ .
Point elasticity. For a curve $Q$ and a price $P$ , $\varepsilon_Q(P)=Q'(P)\,P/Q(P)$ .
Example curves from the source: linear supply $Q(P)=3P-6$ , linear demand $Q(P)=32-2P$ , constant-elasticity supply $Q(P)=5P^{0.5}$ , constant-elasticity demand $Q(P)=3P^{-2}$ .

These definitions are shared by every statement of the mission.

Formalization Note The derivative is Mathlib's deriv (equal to $0$ where $Q$ is not differentiable), and division by $Q(P)=0$ returns $0$ . Real powers are Real.rpow, which is only meaningful here for $P>0$ ; all statements about the isoelastic curves assume $P>0$ .

Definition code

import Mathlib

namespace SupplyDemand

/-- `(p, q)` is a market equilibrium (market-clearing price–quantity pair) for the supply
curve `S` and the demand curve `D`: at the price `p`, the quantity demanded and the quantity
supplied both equal `q`. -/
def IsEquilibrium (S D : ℝ → ℝ) (p q : ℝ) : Prop :=
  D p = q ∧ S p = q

/-- Market (aggregate) curve of a finite family of individual curves `f i`, `i ∈ s`:
at each price the individual quantities are added ("added horizontally"). -/
def marketCurve {ι : Type*} (s : Finset ι) (f : ι → ℝ → ℝ) : ℝ → ℝ :=
  fun p => ∑ i ∈ s, f i p

/-- Point price elasticity of a curve `Q` at the price `P`: `Q'(P) · P / Q(P)`. -/
noncomputable def pointElasticity (Q : ℝ → ℝ) (P : ℝ) : ℝ :=
  deriv Q P * P / Q P

/-- The source's example linear supply function `Q(P) = 3P - 6`. -/
def linearSupply (P : ℝ) : ℝ := 3 * P - 6

/-- The source's example linear demand function `Q(P) = 32 - 2P`. -/
def linearDemand (P : ℝ) : ℝ := 32 - 2 * P

/-- The source's example constant-elasticity supply function `Q(P) = 5 P^{0.5}`. -/
noncomputable def isoelasticSupply (P : ℝ) : ℝ := 5 * P ^ (0.5 : ℝ)

/-- The source's example constant-elasticity demand function `Q(P) = 3 P^{-2}`. -/
noncomputable def isoelasticDemand (P : ℝ) : ℝ := 3 * P ^ (-2 : ℝ)

end SupplyDemand

Source

Wikipedia, "Supply and demand", revision 1378800284, https://en.wikipedia.org/w/index.php?title=Supply_and_demand&oldid=1378800284, sections "Supply schedule", "Demand schedule", "Equilibrium", "Market equilibrium"

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, inside the namespace SupplyDemand, the following objects (everything real-valued, $\mathbb R$ the real numbers).

$\mathrm{IsEquilibrium}(S,D,p,q)$ , for functions $S,D:\mathbb R\to\mathbb R$ and reals $p,q$ , is the proposition " $D(p)=q$ and $S(p)=q$ ". No positivity or monotonicity is built in.
For any index type $\iota$ , a finite set $s\subseteq\iota$ and a family $f:\iota\to(\mathbb R\to\mathbb R)$ , $\mathrm{marketCurve}(s,f)$ is the function $p\mapsto\sum_{i\in s}f_i(p)$ ; for $s=\varnothing$ it is the zero function.
$\mathrm{pointElasticity}(Q,P)=Q'(P)\cdot P/Q(P)$ , where $Q'(P)$ is the derivative of $Q$ at $P$ if $Q$ is differentiable there and $0$ otherwise, and where division by $0$ gives $0$ (so the value is $0$ whenever $Q(P)=0$ ).
$\mathrm{linearSupply}(P)=3P-6$ and $\mathrm{linearDemand}(P)=32-2P$ for all real $P$ (they take negative values for $P<2$ , resp. $P>16$ ).
$\mathrm{isoelasticSupply}(P)=5\,P^{0.5}$ and $\mathrm{isoelasticDemand}(P)=3\,P^{-2}$ , with the real power function $x^y$ ; for $P>0$ this is the usual power, at $P=0$ it gives $0^{0.5}=0$ and $0^{-2}=0$ , and for $P<0$ it gives the library's conventional value $|P|^y\cos(\pi y)$ (for example $(-1)^{0.5}=0$ ) rather than being undefined.

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