The Doeblin chain at large β

At each rate, the uniqueness of the stationary distribution and the convergence to it come from the same three facts as always — a corner at the worst income state, decline above it, and the worst state reachable from everywhere — but at Aiyagari's β = 0.96 each has to come from a route that does not carry 1/(1-β) or 1/(1-βR) in a constant.

• The corner from the Euler inequality (crra_policy_eq_zero_of_euler), whose test is βR · minIncome^(-γ) < (income z₀ + R a₀)^(-γ) — one inequality, no Lipschitz constant.
• Euler-based worst-state decline (policy_lt_self_of_impatient_iid), which holds at every asset level above the constraint given βR < 1 and iid income.
• Cap slack at the fixed point from the minimal MPC (crra_policy_lt_cap_of_minMPC).

Nothing in this file mentions an oscillation bound.

theorem LeanEconomics.IncomeFluctuation.crra_exists_exhaust_of_euler_corner_of_lowest {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hlow : ∀ a ∈ Set.Icc 0 assetCap, ∀ (z : Z), P.consumptionFn z₀ a ≤ P.consumptionFn z a) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState

The exhaustion data at large β, for CRRA, given that consumption is lowest at z₀. The two ways of supplying that are iid income (crra_exists_exhaust_of_euler_corner) and monotone transitions (crra_exists_exhaust_of_euler_corner_monotone).

theorem LeanEconomics.IncomeFluctuation.crra_exists_exhaust_of_euler_corner {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hiid : P.IidIncome) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState

The exhaustion data with iid income.

theorem LeanEconomics.IncomeFluctuation.crra_exists_exhaust_of_euler_corner_monotone {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hmono : P.MonotoneTransitions) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState

The exhaustion data with persistent income: monotone transitions in place of iid, via the income-monotonicity lemma (consumptionFn_le_of_income_le_monotone). The extra iterate-level hypotheses that lemma needs are supplied by the minimal MPC.

theorem LeanEconomics.IncomeFluctuation.crra_existsUnique_isStationary_of_euler_corner {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hiid : P.IidIncome) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) : ∃! μ : MeasureTheory.ProbabilityMeasure P.State, P.IsStationary μ

A unique stationary distribution at large β.

theorem LeanEconomics.IncomeFluctuation.crra_tendsto_pushProb_of_euler_corner {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hiid : P.IidIncome) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) : Filter.Tendsto (fun (m : ℕ) => P.pushProb^[m] μ₀) Filter.atTop (nhds μ)

Convergence to it from any start, Doeblin with the atom at the constraint.

theorem LeanEconomics.IncomeFluctuation.crra_existsUnique_isStationary_of_euler_corner_monotone {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hmono : P.MonotoneTransitions) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) : ∃! μ : MeasureTheory.ProbabilityMeasure P.State, P.IsStationary μ

A unique stationary distribution at large β, with persistent income.

theorem LeanEconomics.IncomeFluctuation.crra_tendsto_pushProb_of_euler_corner_monotone {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hfl : assetFloor = 0) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hmono : P.MonotoneTransitions) (hpc : P.PositiveConsumptionAll) (hthr : (1 - P.minMPC γ) * (P.maxIncome + (1 + P.interest) * assetCap) < assetCap) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {a₀ : ℝ} (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorner : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < (P.income z₀ + (1 + P.interest) * a₀) ^ (-γ)) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) : Filter.Tendsto (fun (m : ℕ) => P.pushProb^[m] μ₀) Filter.atTop (nhds μ)

Convergence to it from any start, with persistent income.