Finite Tauchen earnings for normalized capped-log clearing

The earnings chain discretizes log l' = ρ log l + σ √(1 - ρ²) ε, with standard normal ε, on n + 2 grid points in [-3σ, 3σ]. Its earnings scale c > 0 is arbitrary: no mean-one endowment normalization is imposed. Monotone transitions and positive one-step access to the lowest state follow from monotoneTransitions_of_tauchen and tauchen_pos_zero.

The household has discount 24/25, log utility, no borrowing and a fixed finite asset cap. The rate-uniqueness endpoint uses the prescribed unit-wage normalized clearing equation aggregateCapital μ = normalisedDemand (9/25) (2/25) r, with demand 9 / (16 * (r + 2/25)), and an explicit cap-slack inequality at the larger rate.

A bridge from these household units and the fixed cap to full competitive market clearing for arbitrary earnings scales is not established here. The theorem concerns this explicit normalized clearing equation.

noncomputable def LeanEconomics.aiyagariTauchen (n : ℕ) (ρ σ c cap : ℝ) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hσ : 0 < σ) (hc : 0 < c) (hcap : 0 ≤ cap) : IncomeFluctuation (Fin (n + 2)) 0 cap

A capped log household with a Tauchen earnings chain: β = 0.96, no borrowing, n + 2 grid points on [-3σ, 3σ], persistence ρ, unconditional standard deviation σ and arbitrary positive earnings scale c.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEconomics.aiyagariTauchen_income_strictMono {n : ℕ} {ρ σ c cap : ℝ} {hρ0 : 0 ≤ ρ} {hρ1 : ρ < 1} {hσ : 0 < σ} {hc : 0 < c} {hcap : 0 ≤ cap} : StrictMono (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).income

Income rises strictly with the state.

theorem LeanEconomics.aiyagariTauchen_income_zero {n : ℕ} {ρ σ c cap : ℝ} {hρ0 : 0 ≤ ρ} {hρ1 : ρ < 1} {hσ : 0 < σ} {hc : 0 < c} {hcap : 0 ≤ cap} : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).income 0 = (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).minIncome

The lowest state has the lowest income, which is minIncome.

theorem LeanEconomics.aiyagariTauchen_monotone {n : ℕ} {ρ σ c cap : ℝ} {hρ0 : 0 ≤ ρ} {hρ1 : ρ < 1} {hσ : 0 < σ} {hc : 0 < c} {hcap : 0 ≤ cap} : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).MonotoneTransitions

The chain has monotone transitions.

theorem LeanEconomics.aiyagariTauchen_equilibriumRate_unique_Ioo {n : ℕ} {ρ σ c cap : ℝ} {hρ0 : 0 ≤ ρ} {hρ1 : ρ < 1} {hσ : 0 < σ} {hc : 0 < c} {hcap : 0 ≤ cap} {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Ioo (-2 / 25) (1 / 24)) (h₂ : r₂ ∈ Set.Ioo (-2 / 25) (1 / 24)) (hcapc : 2 * (24 / 25) * (c * Real.exp (3 * σ)) < (1 - 24 / 25 * (1 + max r₁ r₂)) * cap) (hrr₁ : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).RateOK r₁) (hrr₂ : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).RateOK r₂) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).State} (hμ₁ : ((aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).withRate r₁ hrr₁).IsStationary μ₁) (hμ₂ : ((aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).withRate r₂ hrr₂).IsStationary μ₂) (he₁ : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).aggregateCapital μ₁ = normalisedDemand (9 / 25) (2 / 25) r₁) (he₂ : (aiyagariTauchen n ρ σ c cap hρ0 hρ1 hσ hc hcap).aggregateCapital μ₂ = normalisedDemand (9 / 25) (2 / 25) r₂) : r₁ = r₂

Two normalized clearing rates in (-δ, λ) coincide for the finite Tauchen household, for any number of states, ρ ∈ [0, 1), σ > 0 and positive earnings scale, given the cap condition at the larger rate. The hypotheses use the explicit prescribed normalized demand.