Worst-state asset decline from impatience

NaturalAssetBound gets assets to decline from a LINEAR lower bound on consumption, which it can supply only for log utility, and with the very lossy constant exp (-2 β ‖V‖). Its own docstring says what the sharp argument would need: "Getting it needs the Euler equation, hence the envelope condition, hence the machinery that IncomeFluctuationEnvelope supplies only under side conditions." That machinery now exists (hasDerivAt_bellman, euler_ge), and with it the decline condition is not a calibration at all — it is exactly impatience.

The argument, in one line

Let z be the income state at which consumption is LOWEST, and suppose the household does not decumulate there: A = g(a, z) ≥ a. The Euler inequality from saving less is

u'(c(a, z)) ≤ β R · Σ_{z'} π_{z z'} u'(c(A, z')).

Consumption rises with assets and A ≥ a, so c(A, z') ≥ c(a, z') ≥ c(a, z), and marginal utility falls, so every term on the right is at most u'(c(a, z)). The weights sum to one. Hence u'(c(a,z)) ≤ β R · u'(c(a,z)), and since marginal utility is positive, 1 ≤ β R.

So β R < 1 forces decline. No limits, no asymptotic marginal propensity to consume, no calibration — and nothing is asked of the utility beyond a positive, decreasing derivative.

What it costs

Only the Euler inequality's own side conditions: consumption positive at every optimum and the saving strictly below its cap (hslack), which is policyOf_lt_maxSaving once the asset cap is slack. Note the direction — euler_ge comes from the deviation "save LESS", so it needs room BELOW, which is exactly what A ≥ a > assetFloor provides.

Source and scope

Related source: Açıkgöz, April 2016 author draft, Proposition 3, printed page 8 (https://mpra.ub.uni-muenchen.de/71066/1/MPRA_paper_71066.pdf#page=9). That proposition concerns worst-state decline; Proposition 4 on the same page concerns a finite asset bound. The capped variants here have their own explicit positivity, cap-slack and iid or monotone-transition hypotheses; they do not restate the uncapped proposition.

theorem LeanEconomics.IncomeFluctuation.policy_lt_self_of_impatient {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) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hdupos : ∀ (c : ℝ), 0 < c → 0 < du c) (hpos : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, 0 < P.consumptionFn z x) (hslack : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, P.policy (x, z) < P.maxSaving (x, z)) {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (ha0 : assetFloor < a) {z : Z} (hmin : ∀ (z' : Z), P.consumptionFn z a ≤ P.consumptionFn z' a) : P.policy (a, z) < a

Impatience forces decumulation at a state where consumption is lowest.

Which income state consumes least

The Euler argument above runs at the state where consumption is lowest, and the Doeblin construction wants a FIXED state to repeat. The two agree when income is iid: the continuation is then the same function of saving whatever today's state, so the problem depends on the state only through cash on hand, and consumptionFn_mono generalises from two asset levels at one income state to two states with ordered resources.

theorem LeanEconomics.IncomeFluctuation.consumptionFn_mono_of_cont_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {a a' : ℝ} {z₁ z₂ : Z} (hcont : P.cont z₁ = P.cont z₂) (ha : a ∈ Set.Icc assetFloor assetCap) (ha' : a' ∈ Set.Icc assetFloor assetCap) (hres : P.resources (a, z₁) ≤ P.resources (a', z₂)) : P.consumptionFn z₁ a ≤ P.consumptionFn z₂ a'

Consumption rises with resources, across income states as well as asset levels, whenever the two states share a continuation. This is consumptionFn_mono with the state allowed to move: its proof never used z for anything but cont z.

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

Income is iid: the transition probabilities do not depend on today's state.

Equations

• P.IidIncome = ∀ (z₁ z₂ z' : Z), P.transitionMatrix z₁ z' = P.transitionMatrix z₂ z'

theorem LeanEconomics.IncomeFluctuation.cont_eq_of_iid {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hiid : P.IidIncome) (z₁ z₂ : Z) : P.cont z₁ = P.cont z₂

theorem LeanEconomics.IncomeFluctuation.consumptionFn_le_of_income_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hiid : P.IidIncome) {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 an iid income process.

The decline condition, from impatience

Putting the two together: with iid income the lowest-income state is the lowest-consumption state, so the Euler argument runs there, and assets decline at it from EVERY asset level above the borrowing constraint. That is the hypothesis hdecl of exists_exhaust_of_decline, which every witness has been discharging by a numerical calibration. It is impatience.

What is NOT replaced is the corner condition hzero: decline alone gives a strictly falling sequence, and the Doeblin argument needs an ATOM — the constraint has to be reached exactly, not approached. That is a statement about the bottom of the state space, where the Euler equation does not hold, and it stays a calibration.

theorem LeanEconomics.IncomeFluctuation.policy_lt_self_of_impatient_iid {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) (hiid : P.IidIncome) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hdupos : ∀ (c : ℝ), 0 < c → 0 < du c) (hpos : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, 0 < P.consumptionFn z x) (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 in the capped iid model. With iid income and β(1+r) < 1, assets strictly decline at the lowest income state, at every asset level above the borrowing constraint.

theorem LeanEconomics.IncomeFluctuation.exists_exhaust_of_impatient {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) (hiid : P.IidIncome) {du : ℝ → ℝ} (hderiv : ∀ (c : ℝ), 0 < c → HasDerivAt P.u (du c) c) (hanti : AntitoneOn du (Set.Ioi 0)) (hdupos : ∀ (c : ℝ), 0 < c → 0 < du c) (hpos : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, 0 < P.consumptionFn z x) (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₀ : assetFloor < a₀) (hle : a₀ ≤ assetCap) (hzero : ∀ a ∈ Set.Icc assetFloor a₀, P.policy (a, z₀) = assetFloor) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState

The Doeblin exhaustion data, with the decline half free. Only the corner condition is left as a calibration.

CRRA, with the marginal-utility hypotheses discharged

theorem LeanEconomics.IncomeFluctuation.crra_exists_exhaust_of_impatient {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 γ) (hβR : ↑P.discount * (1 + P.interest) < 1) (hiid : P.IidIncome) (hpos : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, 0 < P.consumptionFn z x) (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₀ : assetFloor < a₀) (hle : a₀ ≤ assetCap) (hzero : ∀ a ∈ Set.Icc assetFloor a₀, P.policy (a, z₀) = assetFloor) : ∃ (N : ℕ), (P.gBad z₀)^[N] P.topState = P.botState

Worst-state decline for capped CRRA households. Marginal utility c ^ (-γ) is positive and decreasing for every γ > 0, so impatience is the whole hypothesis.