Consumption Euler equation (two-period problem)

Proved

DSGE.consumption_euler_equation

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

economicseuler-equationoptimization

Consider a consumer with period utility $u : \mathbb R \to \mathbb R$ , discount factor $\beta > 0$ , real interest rate $r$ with $1 + r > 0$ , and wealth $w$ . Consuming $c_0$ today leaves $w - c_0$ to be saved, which pays $c_1 = (1+r)(w - c_0)$ tomorrow; lifetime utility is $U(c_0) = u(c_0) + \beta\, u\big((1+r)(w-c_0)\big)$ . If $c_0 \in (0, w)$ maximises $U$ over $(0, w)$ , and $u$ is differentiable at $c_0$ and at $c_1 = (1+r)(w-c_0)$ , then

u'(c_0) = \beta\,(1+r)\,u'(c_1).

This is the consumption Euler equation that the source describes in words: "our marginal utility from consumption today must equal our marginal utility from consumption in the future, with a weighting parameter that refers to the valuation that we place on the future relative to today." Its log-linearisation is the demand block (dynamic IS curve) of the New Keynesian model.

Formalization Note. The hypotheses $\beta > 0$ and $1 + r > 0$ are the model's standing conventions; the first-order condition itself does not depend on them.

Preamble

import Mathlib

Formal statement

namespace DSGE
theorem consumption_euler_equation (u : ℝ → ℝ) (β r w c₀ : ℝ)
    (hβ : 0 < β) (hr : 0 < 1 + r) (hc₀ : c₀ ∈ Set.Ioo 0 w)
    (hmax : ∀ c ∈ Set.Ioo 0 w,
      u c + β * u ((1 + r) * (w - c)) ≤ u c₀ + β * u ((1 + r) * (w - c₀)))
    (hu₀ : DifferentiableAt ℝ u c₀) (hu₁ : DifferentiableAt ℝ u ((1 + r) * (w - c₀))) :
    deriv u c₀ = β * (1 + r) * deriv u ((1 + r) * (w - c₀)) := by sorry
end DSGE

Source

Wikipedia, "Dynamic stochastic general equilibrium" (uploaded PDF), section "DSGE modeling — Structure" (simplified demand / supply / monetary-policy model) and section "Criticism" (consumption Euler equation paragraph); https://en.wikipedia.org/wiki/Dynamic_stochastic_general_equilibrium (Criticism section: "the central equation for consumption ... marginal utility from consumption today must equal our marginal utility from consumption in the future, with a weighting parameter")

Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements (the mission captain), with full knowledge of the source material and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves or obtain a separate blind read-back.

For every function $u : \mathbb R \to \mathbb R$ and real numbers $\beta, r, w, c_0$ , assume:

$\beta > 0$ and $1 + r > 0$ ;
$0 < c_0 < w$ ;
for every $c$ with $0 < c < w$ : $\; u(c) + \beta\,u\big((1+r)(w-c)\big) \le u(c_0) + \beta\,u\big((1+r)(w-c_0)\big)$ , i.e. $c_0$ maximises $c \mapsto u(c) + \beta u((1+r)(w-c))$ on the open interval $(0,w)$ ;
$u$ is (Fréchet) differentiable at the point $c_0$ and at the point $c_1 := (1+r)(w-c_0)$ .

Then $u'(c_0) = \beta\,(1+r)\,u'(c_1)$ , where $u'$ denotes the derivative of $u$ . No concavity, monotonicity or domain restriction on $u$ is assumed; $u$ is defined on all of $\mathbb R$ . Hypothesis 2 forces $w > 0$ . The hypotheses $\beta>0$ and $1+r>0$ are present but the conclusion would follow without them.

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