Rate uniqueness for normalized capped-log clearing

This file combines rate monotonicity of household saving, monotonicity of stationary mean assets and a strictly decreasing prescribed demand schedule. The log-household constants support discount 24/25.

The prescribed normalized schedule

normalisedDemand α δ r = α / ((1 - α) * (r + δ)) is the capital-to-wage ratio for a Cobb–Douglas firm per unit of effective labor. The clearing equation used here equates this schedule to mean household assets. No mean-one endowment condition or wage/asset-cap scaling bridge to full competitive equilibrium is supplied. The result is uniqueness for this explicit unit-wage normalized clearing problem.

Household conditions

Transitions are monotone in income, and a lowest-income state is reached with positive probability in one step from every state. The Tauchen construction verifies these properties for its arbitrary positive earnings scale. The cap inequality 2β * maxIncome < (1 - β * (1 + rhi)) * cap guarantees the required saving bound across the rate interval; the asset bounds are fixed across that family.

The prescribed normalized demand

noncomputable def LeanEconomics.normalisedDemand (α δ r : ℝ) : ℝ

The prescribed unit-wage normalized demand schedule, per unit of effective labor.

Equations

• LeanEconomics.normalisedDemand α δ r = α / ((1 - α) * (r + δ))

theorem LeanEconomics.normalisedDemand_strictAntiOn {α δ rlo rhi : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hδ : 0 < rlo + δ) : StrictAntiOn (normalisedDemand α δ) (Set.Icc rlo rhi)

Theorem 1 on the interval, by chaining

theorem LeanEconomics.IncomeFluctuation.log_policy_mono_rateFamily {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi ε : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hε : 0 < ε) (hcap : ↑P.discount * P.maxIncome + (↑P.discount * (1 + rhi) + ε) * assetCap < assetCap) (r : ℝ) : r ∈ Set.Icc rlo rhi → ∀ r' ∈ Set.Icc rlo rhi, r ≤ r' → ∀ (s : ℝ × Z), s.1 ∈ Set.Icc 0 assetCap → (P.rateFamily hrlo hlohi r).policy s ≤ (P.rateFamily hrlo hlohi r').policy s

Saving rises with the rate on [rlo, rhi], for log utility. Local comparisons from crra_policy_mono_withRate_of_minMPC chained by monotoneOn_of_local. For log the minimal MPC is 1 - β at every rate, so every cap condition collapses to the one on hcap.

The Doeblin chain on the interval

theorem LeanEconomics.IncomeFluctuation.log_corner_of_top {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi a₀ : ℝ} {z₀ : Z} (hβ : 0 < ↑P.discount) (ha₀ : 0 < a₀) (hcorn : ↑P.discount * (1 + rhi) * (P.income z₀ + (1 + rhi) * a₀) < P.minIncome) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) : ↑(P.withRate r hrr).discount * (1 + (P.withRate r hrr).interest) * (P.withRate r hrr).minIncome ^ (-1) < ((P.withRate r hrr).income z₀ + (1 + (P.withRate r hrr).interest) * a₀) ^ (-1)

The per-rate corner test, from its worst case at the top of the interval. For log the test at rate r is β(1+r)(income z₀ + (1+r) a₀) < minIncome, increasing in r.

theorem LeanEconomics.IncomeFluctuation.log_existsUnique_isStationary {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi a₀ : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + rhi) < 1) (hcap : ↑P.discount * (P.maxIncome + (1 + rhi) * assetCap) < assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorn : ↑P.discount * (1 + rhi) * (P.income z₀ + (1 + rhi) * a₀) < P.minIncome) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) : ∃! μ : MeasureTheory.ProbabilityMeasure P.State, (P.withRate r hrr).IsStationary μ

A unique stationary distribution at every rate in [0, rhi], for log utility.

theorem LeanEconomics.IncomeFluctuation.log_tendsto_pushProb {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi a₀ : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + rhi) < 1) (hcap : ↑P.discount * (P.maxIncome + (1 + rhi) * assetCap) < assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorn : ↑P.discount * (1 + rhi) * (P.income z₀ + (1 + rhi) * a₀) < P.minIncome) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) : Filter.Tendsto (fun (m : ℕ) => (P.withRate r hrr).pushProb^[m] μ₀) Filter.atTop (nhds μ)

Convergence to it from any start, at every rate in [0, rhi].

Theorem 2: capital supply is monotone

theorem LeanEconomics.IncomeFluctuation.log_monotoneOn_capitalSupply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi ε a₀ : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hβR : ↑P.discount * (1 + rhi) < 1) (hε : 0 < ε) (hcap : ↑P.discount * P.maxIncome + (↑P.discount * (1 + rhi) + ε) * assetCap < assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorn : ↑P.discount * (1 + rhi) * (P.income z₀ + (1 + rhi) * a₀) < P.minIncome) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) : MonotoneOn (fun (r : ℝ) => P.aggregateCapital (ν r)) (Set.Icc rlo rhi)

Capital supply rises with the rate on [0, rhi], for log utility, along any selection of stationary distributions. Light's Theorems 1 and 2.

Theorem 3: single crossing

theorem LeanEconomics.IncomeFluctuation.log_equilibriumRate_unique {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi ε a₀ α δ : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hδ : 0 < rlo + δ) (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hβR : ↑P.discount * (1 + rhi) < 1) (hε : 0 < ε) (hcap : ↑P.discount * P.maxIncome + (↑P.discount * (1 + rhi) + ε) * assetCap < assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ha₀ : 0 < a₀) (hle : a₀ ≤ assetCap) (hcorn : ↑P.discount * (1 + rhi) * (P.income z₀ + (1 + rhi) * a₀) < P.minIncome) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Icc rlo rhi) (h₂ : r₂ ∈ Set.Icc rlo rhi) (hrr₁ : P.RateOK r₁) (hrr₂ : P.RateOK r₂) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure P.State} (hμ₁ : (P.withRate r₁ hrr₁).IsStationary μ₁) (hμ₂ : (P.withRate r₂ hrr₂).IsStationary μ₂) (he₁ : P.aggregateCapital μ₁ = normalisedDemand α δ r₁) (he₂ : P.aggregateCapital μ₂ = normalisedDemand α δ r₂) : r₁ = r₂

The normalized clearing rate is unique on [rlo, rhi]. Two rates with stationary household distributions whose mean assets equal the prescribed normalisedDemand α δ r have the same rate, under the stated cap, transition and impatience hypotheses.

With the constants constructed

The interval, the step and the corner level are not primitives of the economy. Given only that the cap clears 2β · maxIncome / (1 - β(1+rhi)), choose the step as half the room under 1 and the corner level as small as the corner test needs.

theorem LeanEconomics.IncomeFluctuation.exists_log_cap_corner {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {R : ℝ} (hβ : 0 < ↑P.discount) (hR : 0 < R) (hcap : 2 * ↑P.discount * P.maxIncome < (1 - ↑P.discount * R) * assetCap) {z₀ : Z} (hmin : P.income z₀ = P.minIncome) : ∃ ε > 0, ∃ a₀ > 0, a₀ ≤ assetCap ∧ ↑P.discount * P.maxIncome + (↑P.discount * R + ε) * assetCap < assetCap ∧ ↑P.discount * R * (P.income z₀ + R * a₀) < P.minIncome

A slack cap supplies a positive comparison step and a corner level meeting both bounds.

theorem LeanEconomics.IncomeFluctuation.log_equilibriumRate_unique_of_cap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi α δ : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hδ : 0 < rlo + δ) (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hβR : ↑P.discount * (1 + rhi) < 1) (hcap : 2 * ↑P.discount * P.maxIncome < (1 - ↑P.discount * (1 + rhi)) * assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Icc rlo rhi) (h₂ : r₂ ∈ Set.Icc rlo rhi) (hrr₁ : P.RateOK r₁) (hrr₂ : P.RateOK r₂) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure P.State} (hμ₁ : (P.withRate r₁ hrr₁).IsStationary μ₁) (hμ₂ : (P.withRate r₂ hrr₂).IsStationary μ₂) (he₁ : P.aggregateCapital μ₁ = normalisedDemand α δ r₁) (he₂ : P.aggregateCapital μ₂ = normalisedDemand α δ r₂) : r₁ = r₂

Uniqueness from one inequality on the cap.

Negative rates

The uniqueness theorems live on [0, rhi]. Below zero the minimal-MPC ceiling on capital supply, β · maxIncome / (1 - β(1+r)), still holds for log utility — κ = 1 - β at every rate — while Cobb--Douglas demand blows up as r ↓ -δ. Where the ceiling is below demand there is no equilibrium.

theorem LeanEconomics.IncomeFluctuation.log_aggregateCapital_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {r : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrr : P.RateOK r) (hβR : ↑P.discount * (1 + r) < 1) (hthr : ↑P.discount * (P.maxIncome + (1 + r) * assetCap) < assetCap) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) : P.aggregateCapital μ ≤ ↑P.discount * P.maxIncome / (1 - ↑P.discount * (1 + r))

The log capital ceiling at any admissible rate with β(1+r) < 1: no sign restriction on r, because κ = 1 - β (minMPC_one).

theorem LeanEconomics.IncomeFluctuation.log_no_equilibrium_of_ceiling {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {α δ r : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrr : P.RateOK r) (hβR : ↑P.discount * (1 + r) < 1) (hthr : ↑P.discount * (P.maxIncome + (1 + r) * assetCap) < assetCap) (hD : ↑P.discount * P.maxIncome / (1 - ↑P.discount * (1 + r)) < normalisedDemand α δ r) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) : P.aggregateCapital μ ≠ normalisedDemand α δ r

No equilibrium where the ceiling is below demand.

Normalized clearing with the Aiyagari (1994) log calibration

The constants are β = 0.96, α = 0.36 and δ = 0.08, with log utility, no borrowing, and monotone earnings transitions reaching a lowest-income state with positive probability in one step. The time-preference rate is λ = 1/0.96 - 1 = 1/24. The theorems concern the prescribed normalized equation on intervals -δ < rlo ≤ rhi < λ; they do not identify it with full competitive market clearing for arbitrary household earnings scales.

theorem LeanEconomics.IncomeFluctuation.aiyagari1994_log_equilibriumRate_unique {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {rlo rhi : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : ↑P.discount = 24 / 25) (hrlo : -2 / 25 < rlo) (hlohi : rlo ≤ rhi) (hlam : rhi < 1 / 24) (hcap : 2 * (24 / 25) * P.maxIncome < (1 - 24 / 25 * (1 + rhi)) * assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Icc rlo rhi) (h₂ : r₂ ∈ Set.Icc rlo rhi) (hrr₁ : P.RateOK r₁) (hrr₂ : P.RateOK r₂) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure P.State} (hμ₁ : (P.withRate r₁ hrr₁).IsStationary μ₁) (hμ₂ : (P.withRate r₂ hrr₂).IsStationary μ₂) (he₁ : P.aggregateCapital μ₁ = normalisedDemand (9 / 25) (2 / 25) r₁) (he₂ : P.aggregateCapital μ₂ = normalisedDemand (9 / 25) (2 / 25) r₂) : r₁ = r₂

The calibrated normalized clearing rate is unique on [rlo, rhi]. The interval is above -δ and below the time-preference rate 1/24. Earnings transitions are monotone and reach a lowest-income state in one step; the asset cap must exceed (48/25) · maxIncome / (1 - (24/25)(1+rhi)).

theorem LeanEconomics.IncomeFluctuation.aiyagari1994_log_equilibriumRate_unique_Ioo {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : ↑P.discount = 24 / 25) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Ioo (-2 / 25) (1 / 24)) (h₂ : r₂ ∈ Set.Ioo (-2 / 25) (1 / 24)) (hcap : 2 * (24 / 25) * P.maxIncome < (1 - 24 / 25 * (1 + max r₁ r₂)) * assetCap) (hrr₁ : P.RateOK r₁) (hrr₂ : P.RateOK r₂) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure P.State} (hμ₁ : (P.withRate r₁ hrr₁).IsStationary μ₁) (hμ₂ : (P.withRate r₂ hrr₂).IsStationary μ₂) (he₁ : P.aggregateCapital μ₁ = normalisedDemand (9 / 25) (2 / 25) r₁) (he₂ : P.aggregateCapital μ₂ = normalisedDemand (9 / 25) (2 / 25) r₂) : r₁ = r₂

Two normalized clearing rates in (-δ, λ) coincide. The interval version is applied to [min r₁ r₂, max r₁ r₂]; the cap condition is required at the larger rate. The clearing hypotheses equate stationary mean household assets to the prescribed normalized demand.

theorem LeanEconomics.IncomeFluctuation.aiyagari1994_log_no_equilibrium_of_ceiling {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {r : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : ↑P.discount = 24 / 25) (hcap : 24 * P.maxIncome < assetCap) (hlo : -2 / 25 < r) (hr0 : r ≤ 0) (hrr : P.RateOK r) (hD : 24 / 25 * P.maxIncome * (r + 2 / 25) < 9 / 16 * (1 - 24 / 25 * (1 + r))) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) : P.aggregateCapital μ ≠ normalisedDemand (9 / 25) (2 / 25) r

No normalized clearing at a negative rate where the saving ceiling is below demand. The ceiling–demand inequality uses the calibrated constants and is polynomial in r and maxIncome, so it can be checked for any earnings grid.

theorem LeanEconomics.IncomeFluctuation.aiyagari1994_log_no_equilibrium_below {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {r : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : ↑P.discount = 24 / 25) (hcap : 24 * P.maxIncome < assetCap) (hmax : P.maxIncome ≤ 3 / 2) (hr : r ∈ Set.Ioc (-2 / 25) (-1 / 20)) (hrr : P.RateOK r) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) : P.aggregateCapital μ ≠ normalisedDemand (9 / 25) (2 / 25) r

No normalized clearing on (-δ, -1/20] when household income is at most 3/2 and the stated asset-cap bound holds. The income bound is an explicit hypothesis in household units; it is not inferred from a mean-one endowment normalization.