The firm side

exists_aiyagari_equilibrium takes any continuous capital demand schedule. This file supplies one that is DERIVED from a production function rather than posited, so the equilibrium theorem becomes a statement about a model rather than about a schedule.

The technology is Cobb–Douglas with α = 1/2, one unit of labour and total factor productivity A, so output is A √K and the marginal product of capital is A / (2√K). Setting the net marginal product equal to the interest rate,

A / (2√K) - δ = r,

and solving gives K = A² / (4(r+δ)²). capitalDemand_marginalProduct checks that the solution really does satisfy the first-order condition, which is what stops the formula from being an arbitrary decreasing function with a suggestive name.

Productivity is a PARAMETER rather than fixed at one because the demand schedule otherwise carries a scale the household side has to be stretched to meet. exists_firm_of_bounds is what that buys: given any rate interval and any two-sided bound on capital supply, some firm meets it there. The firm can be calibrated to the households rather than the other way round.

α = 1/2 is chosen so the inversion is algebraic. A general exponent would need rpow and would change nothing conceptually.

What this does and does not close

Equilibrium needs excess demand to change sign across [rlo, rhi]. The LOW end is now a theorem: capital demand diverges as r approaches -δ, while capital supply can never exceed the asset cap, so capitalDemand 1 δ rlo ≥ assetCap ≥ S rlo for rlo close enough to -δ.

The high-end sign inequality requires positive household capital supply. This module exposes that condition; the later PositiveCapital and SignChange modules provide lower bounds and calibrate the firm under their additional hypotheses. The uniformly impatient NonVacuity household alone has zero stationary capital supply and does not discharge it.

noncomputable def LeanEconomics.capitalDemand (A δ r : ℝ) : ℝ

Capital demand from a Cobb–Douglas firm with α = 1/2, unit labour and productivity A: the capital stock at which the net marginal product equals r.

Equations

• LeanEconomics.capitalDemand A δ r = A ^ 2 / (4 * (r + δ) ^ 2)

theorem LeanEconomics.capitalDemand_marginalProduct {A δ r : ℝ} (hA : 0 < A) (h : 0 < r + δ) : A / (2 * √(capitalDemand A δ r)) - δ = r

The demand schedule solves the firm's first-order condition.

theorem LeanEconomics.capitalDemand_pos {A δ r : ℝ} (hA : 0 < A) (h : 0 < r + δ) : 0 < capitalDemand A δ r

theorem LeanEconomics.continuousOn_capitalDemand {A δ rlo rhi : ℝ} (h : 0 < rlo + δ) : ContinuousOn (capitalDemand A δ) (Set.Icc rlo rhi)

theorem LeanEconomics.capitalDemand_antitoneOn {A δ rlo rhi : ℝ} (h : 0 < rlo + δ) : AntitoneOn (capitalDemand A δ) (Set.Icc rlo rhi)

Capital demand falls as the interest rate rises.

theorem LeanEconomics.exists_capitalDemand_ge (δ : ℝ) {M : ℝ} (hM : 0 ≤ M) : ∃ (rlo : ℝ), 0 < rlo + δ ∧ M ≤ capitalDemand 1 δ rlo

Capital demand diverges as the rate approaches -δ. Given any bound -- in particular the asset cap, which capital supply can never exceed -- some admissible rate demands more.

Reading the two sides of the sign change off the technology

exists_capitalDemand_ge and exists_capitalDemand_le FIND a rate at which demand clears a bound. The two lemmas here do the opposite and more useful thing: given the rate, they say what the technology has to satisfy. Both are the same inequality 4(r+δ)²K ≤ A² read in the two directions, which in root form is 2(r+δ)√K ≤ A — the marginal product of K units at rate r.

theorem LeanEconomics.le_capitalDemand_of_sq {A δ r K : ℝ} (hr : 0 < r + δ) (h : 4 * (r + δ) ^ 2 * K ≤ A ^ 2) : K ≤ capitalDemand A δ r

The technology is productive enough to demand K at rate r. In root form, 2(r+δ)√K ≤ A.

theorem LeanEconomics.capitalDemand_le_of_sq {A δ r K : ℝ} (hr : 0 < r + δ) (h : A ^ 2 ≤ 4 * (r + δ) ^ 2 * K) : capitalDemand A δ r ≤ K

The technology is weak enough to demand no more than K at rate r. In root form, A ≤ 2(r+δ)√K.

The implied rate

Equilibrium is often stated the other way round: a rate r induces a capital stock, the capital stock induces a marginal product, and equilibrium is where the induced rate returns r. That is the same condition — impliedRate inverts capitalDemand — and capitalDemand_eq_iff says so.

noncomputable def LeanEconomics.impliedRate (A δ K : ℝ) : ℝ

The net marginal product of capital at stock K: the rate a firm holding K would pay.

Equations

• LeanEconomics.impliedRate A δ K = A / (2 * √K) - δ

theorem LeanEconomics.capitalDemand_eq_iff {A δ r K : ℝ} (hA : 0 < A) (hr : 0 < r + δ) (hK : 0 < K) : K = capitalDemand A δ r ↔ impliedRate A δ K = r

impliedRate inverts capitalDemand. Demanding K at rate r is the same as K implying r.

theorem LeanEconomics.isAiyagariEquilibrium_iff_impliedRate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} {Pf : ℝ → IncomeFluctuation Z assetFloor assetCap} {A δ r : ℝ} (hA : 0 < A) (hr : 0 < r + δ) : IsAiyagariEquilibrium Pf (capitalDemand A δ) r ↔ ∃ (μ : MeasureTheory.ProbabilityMeasure (Pf r).State), (Pf r).IsStationary μ ∧ 0 < (Pf r).aggregateCapital μ ∧ impliedRate A δ ((Pf r).aggregateCapital μ) = r

Equilibrium in implied-rate form. A rate is an equilibrium exactly when the capital its households hold implies it back.

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

Capital supply never exceeds the asset cap, because every household's assets are capped. This is what makes the low end of the sign change a theorem.

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

Capital supply never falls below the borrowing limit.

theorem LeanEconomics.IncomeFluctuation.exists_rate_capitalDemand_ge {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (δ : ℝ) (μ : MeasureTheory.ProbabilityMeasure P.State) : ∃ (rlo : ℝ), 0 < rlo + δ ∧ P.aggregateCapital μ ≤ capitalDemand 1 δ rlo

The low end of the sign change is a theorem.