Aiyagari stationary equilibrium

An interest rate at which the capital households choose to hold equals the capital firms want to employ.

Aggregation is the easy half and is done here in full: mean assets under the agent distribution is the integral of the asset coordinate, which is a BOUNDED CONTINUOUS function on the compact state space, so aggregate capital is weakly continuous in the distribution. That is the one place the compactness of the state space pays off directly, and it means no separate uniform-integrability argument is needed.

The firm side is left abstract: any continuous capital demand schedule D will do, so a Cobb-Douglas firm with depreciation is one instance among many, and nothing here depends on which.

This module takes continuity of capital supply as an explicit hypothesis. The later AiyagariContinuity module proves it for a fixed-cap, zero-borrowing-floor rate family from a stationary selection that is unique at each rate; its equilibrium theorem also requires a continuous demand schedule and opposite signs of excess demand at the interval endpoints.

Aggregation

theorem LeanEconomics.IncomeFluctuation.continuous_assetCoord {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Continuous fun (s : P.State) => ↑s.1

theorem LeanEconomics.IncomeFluctuation.norm_assetCoord_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : ‖↑s.1‖ ≤ |assetFloor| + |assetCap|

noncomputable def LeanEconomics.IncomeFluctuation.assetCoord {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : BoundedContinuousFunction P.State ℝ

The asset coordinate, as a bounded continuous function. Boundedness is exactly the asset cap, and continuity is immediate; together they are what make aggregate capital behave well under weak convergence.

Equations

• P.assetCoord = BoundedContinuousFunction.ofNormedAddCommGroup (fun (s : P.State) => ↑s.1) ⋯ (|assetFloor| + |assetCap|) ⋯

@[simp]

theorem LeanEconomics.IncomeFluctuation.assetCoord_apply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : P.assetCoord s = ↑s.1

noncomputable def LeanEconomics.IncomeFluctuation.aggregateCapital {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] (μ : MeasureTheory.ProbabilityMeasure P.State) : ℝ

Aggregate capital: mean assets under an agent distribution.

Equations

• P.aggregateCapital μ = ∫ (s : P.State), P.assetCoord s ∂↑μ

theorem LeanEconomics.IncomeFluctuation.continuous_aggregateCapital {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] : Continuous P.aggregateCapital

Aggregation is weakly continuous. The asset coordinate is bounded and continuous, so this is exactly what the weak topology is designed to give.

Equilibrium

def LeanEconomics.IsAiyagariEquilibrium {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (Pf : ℝ → IncomeFluctuation Z assetFloor assetCap) (D : ℝ → ℝ) (r : ℝ) : Prop

An Aiyagari stationary equilibrium at interest rate r: the household problem Pf r has a stationary agent distribution whose aggregate capital equals the capital demanded at that rate.

Equations

• LeanEconomics.IsAiyagariEquilibrium Pf D r = ∃ (μ : MeasureTheory.ProbabilityMeasure (Pf r).State), (Pf r).IsStationary μ ∧ (Pf r).aggregateCapital μ = D r

theorem LeanEconomics.exists_aiyagari_equilibrium {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} {Pf : ℝ → IncomeFluctuation Z assetFloor assetCap} {D S : ℝ → ℝ} {rlo rhi : ℝ} (hle : rlo ≤ rhi) (hS : ∀ (r : ℝ), ∃ (μ : MeasureTheory.ProbabilityMeasure (Pf r).State), (Pf r).IsStationary μ ∧ (Pf r).aggregateCapital μ = S r) (hScont : ContinuousOn S (Set.Icc rlo rhi)) (hDcont : ContinuousOn D (Set.Icc rlo rhi)) (hlo : S rlo ≤ D rlo) (hhi : D rhi ≤ S rhi) : ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium Pf D r

Existence of an Aiyagari stationary equilibrium.

Given a capital supply schedule S that is realised by a stationary distribution at every interest rate and is continuous, and any continuous capital demand schedule D, a rate at which the two agree exists as soon as excess demand changes sign across the interval.

Uniqueness of the stationary distribution is what makes S a FUNCTION of r rather than a correspondence, and that is what allows the intermediate value theorem to close the argument in place of a fixed point theorem for correspondences -- Mathlib has no Kakutani.

Rate continuity and the remaining hypotheses

IncomeFluctuation Z assetFloor assetCap takes the asset bounds as parameters. Fixing them across a rate family gives a common state space for its stationary distributions.

For a zero borrowing floor, IncomeFluctuation.continuousOn_capitalSupply in Equilibrium/AiyagariContinuity.lean proves rate continuity from a selection of stationary distributions and uniqueness at every rate of a closed interval. Its IncomeFluctuation.exists_equilibrium_of_selection then applies the intermediate value theorem, assuming a continuous capital-demand schedule and endpoint sign inequalities. The stationary selection, its uniqueness and the endpoint inequalities remain explicit hypotheses of that result. The more abstract theorem in this file also allows other fixed borrowing floors, while taking continuity of the realised supply schedule as a hypothesis.