Uniqueness of the stationary agent distribution

A Doeblin argument, made available by the borrowing constraint.

The asset transition is deterministic given the shock, so the laws started from two different asset levels have disjoint supports and no minorization against a spread-out measure can hold. An ATOM escapes that obstruction: if a long enough run of bad income shocks drives every household to exactly the borrowing constraint, then every N-step law charges the single point s₀ = (0, z₀) with probability at least ε, and that is a genuine Doeblin condition.

The contraction is run on the function side, where markovOp already lives, rather than on signed measures. The oscillation supF h - infF h contracts by 1 - ε every N steps, so for two stationary distributions ∫ h dμ - ∫ h dν is squeezed to zero for every bounded continuous h, and extensionality finishes.

The range of a bounded continuous function

theorem LeanEconomics.IncomeFluctuation.bddAbove_range {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : BddAbove (Set.range ⇑h)

theorem LeanEconomics.IncomeFluctuation.bddBelow_range {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : BddBelow (Set.range ⇑h)

noncomputable def LeanEconomics.IncomeFluctuation.supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : ℝ

The supremum of a bounded continuous function on the state space.

Equations

• P.supF h = ⨆ (s : P.State), h s

noncomputable def LeanEconomics.IncomeFluctuation.infF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : ℝ

The infimum of a bounded continuous function on the state space.

Equations

• P.infF h = ⨅ (s : P.State), h s

theorem LeanEconomics.IncomeFluctuation.le_supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : h s ≤ P.supF h

theorem LeanEconomics.IncomeFluctuation.infF_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : P.infF h ≤ h s

theorem LeanEconomics.IncomeFluctuation.infF_le_supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : P.infF h ≤ P.supF h

theorem LeanEconomics.IncomeFluctuation.sup_sub_inf_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {h : BoundedContinuousFunction P.State ℝ} {C : ℝ} (hC : ∀ (s t : P.State), h s - h t ≤ C) : P.supF h - P.infF h ≤ C

If every gap is at most C, the oscillation is at most C.

The Markov operator preserves bounds

theorem LeanEconomics.IncomeFluctuation.infF_le_markovOp {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : P.infF h ≤ (P.markovOp h) s

theorem LeanEconomics.IncomeFluctuation.markovOp_le_supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : (P.markovOp h) s ≤ P.supF h

theorem LeanEconomics.IncomeFluctuation.infF_le_iterate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (n : ℕ) (s : P.State) : P.infF h ≤ (P.markovOp^[n] h) s

theorem LeanEconomics.IncomeFluctuation.iterate_le_supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (n : ℕ) (s : P.State) : (P.markovOp^[n] h) s ≤ P.supF h

The Doeblin minorization

noncomputable def LeanEconomics.IncomeFluctuation.badStep {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z₀ : Z) (s : P.State) : P.State

One period under the worst income shock z₀.

Equations

• P.badStep z₀ s = P.nextState s z₀

theorem LeanEconomics.IncomeFluctuation.iterate_lower {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {p₀ : ℝ} (hp0 : 0 ≤ p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (h : BoundedContinuousFunction P.State ℝ) (n : ℕ) (s : P.State) : p₀ ^ n * h ((P.badStep z₀)^[n] s) + (1 - p₀ ^ n) * P.infF h ≤ (P.markovOp^[n] h) s

Minorization, lower half. After n periods, a share p₀ⁿ of the mass sits at the state reached by n consecutive bad shocks, and the rest is worth at least infF h.

theorem LeanEconomics.IncomeFluctuation.iterate_upper {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {p₀ : ℝ} (hp0 : 0 ≤ p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (h : BoundedContinuousFunction P.State ℝ) (n : ℕ) (s : P.State) : (P.markovOp^[n] h) s ≤ p₀ ^ n * h ((P.badStep z₀)^[n] s) + (1 - p₀ ^ n) * P.supF h

Minorization, upper half.

The oscillation contracts

theorem LeanEconomics.IncomeFluctuation.osc_markovOp_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {s₀ : P.State} {p₀ : ℝ} {N : ℕ} (hp0 : 0 ≤ p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (hbad : ∀ (s : P.State), (P.badStep z₀)^[N] s = s₀) (h : BoundedContinuousFunction P.State ℝ) : P.supF (P.markovOp^[N] h) - P.infF (P.markovOp^[N] h) ≤ (1 - p₀ ^ N) * (P.supF h - P.infF h)

One Doeblin cycle contracts the oscillation by the factor 1 - p₀ᴺ. Both households are compared against the same value h s₀, which is what hbad buys.

theorem LeanEconomics.IncomeFluctuation.osc_cycle_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {s₀ : P.State} {p₀ : ℝ} {N : ℕ} (hp0 : 0 ≤ p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (hbad : ∀ (s : P.State), (P.badStep z₀)^[N] s = s₀) (k : ℕ) (h : BoundedContinuousFunction P.State ℝ) : P.supF (P.markovOp^[N]^[k] h) - P.infF (P.markovOp^[N]^[k] h) ≤ (1 - p₀ ^ N) ^ k * (P.supF h - P.infF h)

Stationarity is preserved along the iteration

theorem LeanEconomics.IncomeFluctuation.integral_iterate_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {μ : MeasureTheory.Measure P.State} [MeasureTheory.IsProbabilityMeasure μ] (hμ : P.push μ = μ) (n : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), (P.markovOp^[n] h) s ∂μ = ∫ (s : P.State), h s ∂μ

theorem LeanEconomics.IncomeFluctuation.integral_cycle_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {μ : MeasureTheory.Measure P.State} [MeasureTheory.IsProbabilityMeasure μ] (hμ : P.push μ = μ) (N k : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), (P.markovOp^[N]^[k] h) s ∂μ = ∫ (s : P.State), h s ∂μ

theorem LeanEconomics.IncomeFluctuation.integral_le_supF {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure μ] (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), h s ∂μ ≤ P.supF h

theorem LeanEconomics.IncomeFluctuation.infF_le_integral {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure μ] (h : BoundedContinuousFunction P.State ℝ) : P.infF h ≤ ∫ (s : P.State), h s ∂μ

Uniqueness

theorem LeanEconomics.IncomeFluctuation.stationary_unique {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {z₀ : Z} {s₀ : P.State} {p₀ : ℝ} {N : ℕ} (hp0 : 0 < p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (hbad : ∀ (s : P.State), (P.badStep z₀)^[N] s = s₀) {μ ν : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) (hν : P.IsStationary ν) : μ = ν

The stationary agent distribution is unique, given a Doeblin condition: some income state z₀ is always reachable with probability at least p₀ > 0, and N consecutive z₀ shocks drive every state to the single state s₀.

In the income fluctuation problem s₀ is the borrowing constraint. The atom is what makes a Doeblin argument possible at all: the asset transition is deterministic, so laws started from different assets have disjoint supports and no minorization against a spread-out measure can hold — but they all charge the constraint.

Discharging the Doeblin condition in the model

The abstract condition asks that N bad shocks drive every state to the borrowing constraint. Monotonicity of the policy reduces that to the single worst case: if the richest household is exhausted in N periods, everyone is, because the asset map is increasing and bounded below by zero.

noncomputable def LeanEconomics.IncomeFluctuation.gBad {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z₀ : Z) (x : ↑(Set.Icc assetFloor assetCap)) : ↑(Set.Icc assetFloor assetCap)

The asset map under the worst income shock.

Equations

• P.gBad z₀ x = P.nextAssets (x, z₀)

theorem LeanEconomics.IncomeFluctuation.gBad_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z₀ : Z) : Monotone (P.gBad z₀)

def LeanEconomics.IncomeFluctuation.topState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ↑(Set.Icc assetFloor assetCap)

The richest state.

Equations

• P.topState = ⟨assetCap, ⋯⟩

theorem LeanEconomics.IncomeFluctuation.le_topState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (x : ↑(Set.Icc assetFloor assetCap)) : x ≤ P.topState

def LeanEconomics.IncomeFluctuation.botState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ↑(Set.Icc assetFloor assetCap)

The bottom state: the borrowing constraint.

Equations

• P.botState = ⟨assetFloor, ⋯⟩

theorem LeanEconomics.IncomeFluctuation.botState_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (x : ↑(Set.Icc assetFloor assetCap)) : P.botState ≤ x

theorem LeanEconomics.IncomeFluctuation.gBad_iterate_eq_bot {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {N : ℕ} (hexh : (P.gBad z₀)^[N] P.topState = P.botState) (x : ↑(Set.Icc assetFloor assetCap)) : (P.gBad z₀)^[N] x = P.botState

Monotonicity reduces exhaustion to the worst case.

theorem LeanEconomics.IncomeFluctuation.badStep_iterate_succ {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z₀ : Z) (n : ℕ) (s : P.State) : (P.badStep z₀)^[n + 1] s = ((P.gBad z₀)^[n] (P.nextAssets s), z₀)

theorem LeanEconomics.IncomeFluctuation.badStep_iterate_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {N : ℕ} (hexh : (P.gBad z₀)^[N] P.topState = P.botState) (s : P.State) : (P.badStep z₀)^[N + 1] s = (P.botState, z₀)

The Doeblin condition holds once the richest household is exhausted by N bad shocks: after one more period every state has collapsed to the borrowing constraint.

theorem LeanEconomics.IncomeFluctuation.stationary_unique_of_exhausts {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {z₀ : Z} {N : ℕ} (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (hexh : (P.gBad z₀)^[N] P.topState = P.botState) {μ ν : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) (hν : P.IsStationary ν) : μ = ν

Uniqueness of the stationary agent distribution for the income fluctuation problem.

The two economic assumptions are that the worst income state z₀ is reachable from every income state (hreach), and that a household starting with the maximum assets is driven to the borrowing constraint by N consecutive draws of z₀ (hexh). Monotonicity of the policy then carries the second from the richest household to every household.

theorem LeanEconomics.IncomeFluctuation.existsUnique_isStationary {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {z₀ : Z} {N : ℕ} (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (hexh : (P.gBad z₀)^[N] P.topState = P.botState) : ∃! μ : MeasureTheory.ProbabilityMeasure P.State, P.IsStationary μ

Existence and uniqueness together.

Convergence

Uniqueness says there is one stationary distribution; convergence says the economy finds it. The same oscillation contraction gives both. Iterating the operator flattens any test function geometrically, and a flat test function cannot tell two distributions apart, so the iterates of ANY initial distribution become indistinguishable from the stationary one.

This is what makes the stationary distribution computable rather than merely unique: it is the limit of iterating from wherever you start.

theorem LeanEconomics.IncomeFluctuation.integral_pushProb_iterate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.ProbabilityMeasure P.State) (m : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), h s ∂↑(P.pushProb^[m] μ) = ∫ (s : P.State), (P.markovOp^[m] h) s ∂↑μ

theorem LeanEconomics.IncomeFluctuation.osc_iterate_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (j : ℕ) : P.supF (P.markovOp^[j] h) - P.infF (P.markovOp^[j] h) ≤ P.supF h - P.infF h

Oscillation cannot grow under the operator.

theorem LeanEconomics.IncomeFluctuation.tendsto_osc_iterate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {s₀ : P.State} {p₀ : ℝ} {N : ℕ} (hp0 : 0 < p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (hbad : ∀ (s : P.State), (P.badStep z₀)^[N] s = s₀) (h : BoundedContinuousFunction P.State ℝ) : Filter.Tendsto (fun (m : ℕ) => P.supF (P.markovOp^[m] h) - P.infF (P.markovOp^[m] h)) Filter.atTop (nhds 0)

The oscillation of an iterated test function vanishes.

theorem LeanEconomics.IncomeFluctuation.tendsto_pushProb_iterate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] {z₀ : Z} {s₀ : P.State} {p₀ : ℝ} {N : ℕ} (hp0 : 0 < p₀) (hp : ∀ (s : P.State), p₀ ≤ P.prob s z₀) (hbad : ∀ (s : P.State), (P.badStep z₀)^[N] s = s₀) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) : Filter.Tendsto (fun (m : ℕ) => P.pushProb^[m] μ₀) Filter.atTop (nhds μ)

Convergence to the stationary distribution. From any starting point, the iterates of the distribution operator converge weakly to the stationary distribution.

Exhaustion from strict dissaving

badStep_iterate_eq takes exhaustion as a hypothesis in the awkward form gBad^[N] top = bot -- an exact hit on the borrowing constraint after a specified number of periods. That is hard to check directly, and in the earlier calibrations it was obtained only by making the policy identically zero.

In Açıkgöz's April 2016 author draft, Proposition 5 (printed page 9; proof in Appendix E, printed page 32) uses two natural facts: the constraint binds near zero, and assets strictly decline above that at the worst income state. A continuous strictly declining map on a compact interval has a UNIFORM minimum decline, so finitely many periods carry the richest household below the threshold, and one more step pins it to the constraint.

In that edition, Proposition 3 (printed page 8) supplies worst-state decline, while Proposition 4 (the same page) supplies a finite asset bound. The source is https://mpra.ub.uni-muenchen.de/71066/1/MPRA_paper_71066.pdf. The lemma below uses only continuity, binding near the constraint and strict decline on an already compact interval; the Euler arguments establishing these inputs appear separately.

theorem LeanEconomics.IncomeFluctuation.exists_exhaust_of_decline {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z₀ : Z} {a₀ : ℝ} (ha₀ : assetFloor < a₀) (hle : a₀ ≤ assetCap) (hzero : ∀ a ∈ Set.Icc assetFloor a₀, P.policy (a, z₀) = assetFloor) (hdecl : ∀ a ∈ Set.Icc a₀ assetCap, P.policy (a, z₀) < a) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState