Capital supply is continuous, and the equilibrium theorem applies

exists_aiyagari_equilibrium has carried one hypothesis since it was proved: that capital supply moves continuously with the interest rate. This file discharges it.

Aggregation turns out not to depend on the rate at all -- the asset coordinate is the asset coordinate whatever the rate, and aggregateCapital is equal across rates by rfl -- so all the rate dependence sits in the stationary distribution, and tendsto_stationary supplies it. Capital supply is then a continuous function composed with a convergent selection.

The family is indexed by the CLAMPED rate, so that a household problem is defined at every real number while agreeing with the intended one on [rlo, rhi]. Without that the family would need a proof of 0 < 1 + r at every real r, which is false.

noncomputable def LeanEconomics.IncomeFluctuation.rateFamily {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (r : ℝ) : IncomeFluctuation Z 0 assetCap

The household problem at the clamped rate, defined at every real number.

Equations

• P.rateFamily hrlo hle r = P.withRate (LeanEconomics.clampRate rlo rhi r) ⋯

theorem LeanEconomics.IncomeFluctuation.rateFamily_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) : P.rateFamily hrlo hle r = P.withRate r hrr

theorem LeanEconomics.IncomeFluctuation.continuousOn_capitalSupply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate r hrr).IsStationary μ → μ = ν r) : ContinuousOn (fun (r : ℝ) => P.aggregateCapital (ν r)) (Set.Icc rlo rhi)

Capital supply is continuous in the interest rate.

theorem LeanEconomics.IncomeFluctuation.exists_equilibrium_of_selection {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate r hrr).IsStationary μ → μ = ν r) (D : ℝ → ℝ) (hD : ContinuousOn D (Set.Icc rlo rhi)) (hlo : P.aggregateCapital (ν rlo) ≤ D rlo) (hhi : D rhi ≤ P.aggregateCapital (ν rhi)) : ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium (P.rateFamily hrlo hle) D r

An Aiyagari stationary equilibrium exists, with nothing assumed about the household side beyond a selection of stationary distributions that is unique at each rate.

Compared with exists_aiyagari_equilibrium, the continuity of capital supply is no longer a hypothesis: it is proved, from continuity of the policy in the rate and weak continuity of aggregation. What remains assumed is the firm side -- any continuous demand schedule -- and that excess demand changes sign, which is where the economics of the calibration enters.