Comparative statics of supply and demand

Proved

SupplyDemand.comparative_statics

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

economicsmicroeconomicssupply-and-demand

Fix a set $I\subseteq\mathbb R$ of admissible prices. Supply curves are assumed strictly increasing on $I$ and demand curves strictly decreasing on $I$ ; all equilibrium prices are assumed to lie in $I$ .

Demand shift. If $D_1(p)<D_2(p)$ for all $p\in I$ , $(p_1,q_1)$ is an equilibrium of $(S,D_1)$ and $(p_2,q_2)$ is an equilibrium of $(S,D_2)$ , then

p_1<p_2\quad\text{and}\quad q_1<q_2.

Supply shift. If $S_1(p)<S_2(p)$ for all $p\in I$ , $(p_1,q_1)$ is an equilibrium of $(S_1,D)$ and $(p_2,q_2)$ is an equilibrium of $(S_2,D)$ , then

p_2<p_1\quad\text{and}\quad q_1<q_2.

An increase in demand raises both equilibrium price and quantity; an increase in supply lowers the price and raises the quantity. The statements for decreases are obtained by exchanging the indices.

Formalization Note Curves are functions $\mathbb R\to\mathbb R$ ; the slope assumptions are imposed on an arbitrary set $I$ of admissible prices, and all equilibrium prices are assumed to lie in $I$ .

Preamble

import Mathlib
import Definitions.Def_SupplyDemand_Model

Formal statement

namespace SupplyDemand

theorem comparative_statics (I : Set ℝ) :
    (∀ (S D₁ D₂ : ℝ → ℝ), StrictMonoOn S I → StrictAntiOn D₁ I → StrictAntiOn D₂ I →
      (∀ p ∈ I, D₁ p < D₂ p) →
      ∀ p₁ q₁ p₂ q₂ : ℝ, p₁ ∈ I → p₂ ∈ I →
        IsEquilibrium S D₁ p₁ q₁ → IsEquilibrium S D₂ p₂ q₂ →
        p₁ < p₂ ∧ q₁ < q₂) ∧
    (∀ (S₁ S₂ D : ℝ → ℝ), StrictMonoOn S₁ I → StrictMonoOn S₂ I → StrictAntiOn D I →
      (∀ p ∈ I, S₁ p < S₂ p) →
      ∀ p₁ q₁ p₂ q₂ : ℝ, p₁ ∈ I → p₂ ∈ I →
        IsEquilibrium S₁ D p₁ q₁ → IsEquilibrium S₂ D p₂ q₂ →
        p₂ < p₁ ∧ q₁ < q₂) := by sorry

end SupplyDemand

Source

Wikipedia, "Supply and demand", revision 1378800284, https://en.wikipedia.org/w/index.php?title=Supply_and_demand&oldid=1378800284, section "Changes in market equilibrium", "Demand curve shifts", "Supply curve shifts"

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.

For every set $I\subseteq\mathbb R$ the statement asserts the conjunction of two universally quantified claims.

(1) For all functions $S,D_1,D_2:\mathbb R\to\mathbb R$ : if $S$ is strictly increasing on $I$ , $D_1$ and $D_2$ are strictly decreasing on $I$ , and $D_1(p)<D_2(p)$ for every $p\in I$ , then for all reals $p_1,q_1,p_2,q_2$ with $p_1\in I$ , $p_2\in I$ , $D_1(p_1)=q_1$ , $S(p_1)=q_1$ , $D_2(p_2)=q_2$ , $S(p_2)=q_2$ , one has $p_1<p_2$ and $q_1<q_2$ .

(2) For all functions $S_1,S_2,D:\mathbb R\to\mathbb R$ : if $S_1$ and $S_2$ are strictly increasing on $I$ , $D$ is strictly decreasing on $I$ , and $S_1(p)<S_2(p)$ for every $p\in I$ , then for all reals $p_1,q_1,p_2,q_2$ with $p_1,p_2\in I$ , $D(p_1)=q_1$ , $S_1(p_1)=q_1$ , $D(p_2)=q_2$ , $S_2(p_2)=q_2$ , one has $p_2<p_1$ and $q_1<q_2$ .

Existence of equilibria is neither assumed nor asserted; all inequalities are strict.

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