The isoelastic curves have constant elasticity 0.5 and −2

Proved

SupplyDemand.isoelastic_constant_elasticity

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

economicsmicroeconomicssupply-and-demand

For every price $P>0$ , the point price elasticity $\varepsilon_Q(P)=Q'(P)\,P/Q(P)$ of the source's constant-elasticity curves is constant:

\varepsilon_{S}(P)=0.5\quad\text{for } S(P)=5P^{0.5},\qquad \varepsilon_{D}(P)=-2\quad\text{for } D(P)=3P^{-2}.

This justifies the name "constant-elasticity" used in the source.

Preamble

import Mathlib
import Definitions.Def_SupplyDemand_Model

Formal statement

namespace SupplyDemand

theorem isoelastic_constant_elasticity (P : ℝ) (hP : 0 < P) :
    pointElasticity isoelasticSupply P = 0.5 ∧
    pointElasticity isoelasticDemand P = -2 := 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 "Supply schedule" and "Demand schedule" (constant-elasticity specifications)

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 real $P>0$ , the statement asserts: (1) $\dfrac{S'(P)\cdot P}{S(P)}=0.5$ where $S(x)=5x^{0.5}$ ; (2) $\dfrac{D'(P)\cdot P}{D(P)}=-2$ where $D(x)=3x^{-2}$ . Here $S'(P)$ , $D'(P)$ denote the derivative at $P$ (the definition uses $0$ if the function were not differentiable at $P$ , and division by $0$ would give $0$ ).

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