Persistent income: the decline condition from monotone transitions

Açıkgöz's decline argument (policy_lt_self_of_impatient) runs the Euler inequality at the state where consumption is lowest, and needs to know which state that is. With iid income it is the lowest-income state, because every state shares a continuation. With persistent income the continuations differ, and the lowest-income state is still the lowest-consumption state only if its continuation is the STEEPEST — a poor household today expects to be poor tomorrow, so wealth is worth more to it at the margin.

This file proves the property in secant form for a finite income process ordered by income, using induction on Bellman iterates. Related literature: Huggett (1993), The Risk-Free Rate in Heterogeneous-Agent Incomplete-Insurance Economies.

Monotone transitions

The condition is stated by its use: a state with higher income has a transition row that makes every income-antitone function of tomorrow's state smaller in expectation (MonotoneTransitions). For two states it is exactly π(h|h) ≥ π(h|l) (monotoneTransitions_of_two_states); for a Tauchen chain it is first-order stochastic dominance of the rows, which the chain has by construction.

The induction

IncDiffAcrossStates v says the increments of v in assets are antitone in income. It survives the Bellman operator because the envelope derivative is R · u'(c) and consumption at a fixed asset level is increasing in income (consumptionFnOf_le_across_states) — which in turn follows from single crossing: a richer household with a flatter continuation saves less of its extra resources than it receives. The base case is the zero continuation, and the property passes to the value function as a pointwise limit.

The two properties

def LeanEconomics.IncomeFluctuation.MonotoneTransitions {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Prop

Monotone transitions. A higher-income state's transition row makes every income-antitone function of tomorrow's state smaller in expectation: first-order stochastic dominance of the rows, in the income order.

Equations

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

theorem LeanEconomics.IncomeFluctuation.monotoneTransitions_of_iid {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hiid : P.IidIncome) : P.MonotoneTransitions

iid income has monotone transitions, trivially: the rows are all equal.

theorem LeanEconomics.IncomeFluctuation.monotoneTransitions_withRate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} {P : IncomeFluctuation Z 0 assetCap} (hmono : P.MonotoneTransitions) {r : ℝ} (hrr : P.RateOK r) : (P.withRate r hrr).MonotoneTransitions

Changing the rate leaves the income process, hence monotonicity, untouched.

def LeanEconomics.IncomeFluctuation.IncDiffAcrossStates {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : Prop

Increments of v in assets are antitone in income: the secant form of Huggett's v'(a, e_h) ≤ v'(a, e_l).

Equations

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

theorem LeanEconomics.IncomeFluctuation.incDiffAcrossStates_zero {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.IncDiffAcrossStates 0

theorem LeanEconomics.IncomeFluctuation.contOf_sub_le_across_states {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hmono : P.MonotoneTransitions) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : P.IncDiffAcrossStates v) {z₁ z₂ : Z} (hz : P.income z₁ ≤ P.income z₂) {x y : ℝ} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) (hxy : x ≤ y) : P.contOf v z₂ y - P.contOf v z₂ x ≤ P.contOf v z₁ y - P.contOf v z₁ x

The continuation inherits the property, by monotone transitions: the increment v (y, ·) - v (x, ·) is income-antitone, and the poorer state's row weights it more.

Consumption rises with income at a fixed asset level

The exchange argument of consumptionFn_mono_of_cont_eq, with the shared continuation replaced by an ordered pair: the richer state has a flatter continuation as well as more resources, and both push consumption up.

The Bellman step, by the envelope

theorem LeanEconomics.IncomeFluctuation.incDiffAcrossStates_bellman {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hmono : P.MonotoneTransitions) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hv : ConcaveSlices assetFloor assetCap v) (hpc : P.PositiveConsumptionAll) (hslack : ∀ x ∈ Set.Icc assetFloor assetCap, ∀ (z : Z), P.policyOf v (x, z) < assetCap) (hid : P.IncDiffAcrossStates v) : P.IncDiffAcrossStates (P.toExtended.bellman v)

Income-antitone increments, one Bellman step. If v has income-antitone increments, then so does bellman v: the derivative of bellman v (·, z) is R · u'(c_v(·, z)), and consumption at a fixed asset level rises with income.

Along the iteration, and at the fixed point

theorem LeanEconomics.IncomeFluctuation.incDiffAcrossStates_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hmono : P.MonotoneTransitions) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hpc : P.PositiveConsumptionAll) (hslack : ∀ (n : ℕ), ∀ x ∈ Set.Icc assetFloor assetCap, ∀ (z : Z), P.policyOf (P.toExtended.bellman^[n] 0) (x, z) < assetCap) : P.IncDiffAcrossStates P.toExtended.valueFunction

Income-antitone increments at the value function.

theorem LeanEconomics.IncomeFluctuation.consumptionFn_le_of_income_le_monotone {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hmono : P.MonotoneTransitions) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hpc : P.PositiveConsumptionAll) (hslack : ∀ (n : ℕ), ∀ x ∈ Set.Icc assetFloor assetCap, ∀ (z : Z), P.policyOf (P.toExtended.bellman^[n] 0) (x, z) < assetCap) {z₁ z₂ : Z} (hinc : P.income z₁ ≤ P.income z₂) {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) : P.consumptionFn z₁ a ≤ P.consumptionFn z₂ a

Consumption is lowest where income is lowest, for a persistent income process with monotone transitions. The replacement for consumptionFn_le_of_income_le.

theorem LeanEconomics.IncomeFluctuation.policy_lt_self_of_impatient_monotone {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hβR : ↑P.discount * (1 + P.interest) < 1) (hmono : P.MonotoneTransitions) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hdupos : ∀ (c : ℝ), 0 < c → 0 < du c) (hpc : P.PositiveConsumptionAll) (hslackIt : ∀ (n : ℕ), ∀ x ∈ Set.Icc assetFloor assetCap, ∀ (z : Z), P.policyOf (P.toExtended.bellman^[n] 0) (x, z) < assetCap) (hslack : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, P.policy (x, z) < P.maxSaving (x, z)) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (ha0 : assetFloor < a) : P.policy (a, z₀) < a

Worst-state decline with persistent income. Assets strictly decline at the lowest income state, at every asset level above the borrowing constraint, given β(1+r) < 1 and monotone transitions.

Two states

theorem LeanEconomics.IncomeFluctuation.monotoneTransitions_of_two_states {assetFloor assetCap : ℝ} (P : IncomeFluctuation (Fin 2) assetFloor assetCap) (hinc : P.income 0 ≤ P.income 1) (hπ : P.transitionMatrix 0 1 ≤ P.transitionMatrix 1 1) : P.MonotoneTransitions

Huggett's condition is monotone transitions, for two income states ordered by income: π(h | h) ≥ π(h | l).