The corner condition from the Euler inequality

policy_eq_zero_of_corner_at gets the corner from a LIPSCHITZ bound on the value function, β L < m. The constant L is slopeBound / (1 - βR), and at Aiyagari's β = 0.96 that is several hundred times the true slope, so the test fails by orders of magnitude. This file gets the corner from the Euler inequality instead, and the only thing it asks is βR < 1.

The argument

Two steps, both at the fixed point.

Nobody at the borrowing limit consumes less than the worst income. Take the income state at which consumption at the limit is smallest. If that household were saving, its Euler inequality (euler_ge) would read u'(c) ≤ βR E[u'(c')]; but tomorrow's consumption is at least today's minimum (consumption rises with assets, and assets can only have risen), so u'(c') ≤ u'(c) and u'(c) ≤ βR u'(c), impossible with βR < 1. So the household at the minimum is at the corner, consumes its whole income, and the minimum is at least minIncome.

The corner, state by state. At any state where βR · u'(minIncome) < u'(cash on hand), saving is not optimal: if it were, the Euler inequality and step one would give u'(cash on hand) ≤ u'(c) ≤ βR u'(minIncome). This is the contrapositive of euler_ge.

For log utility the test at the worst income state is a < minIncome (1 - βR) / (βR²): a small but positive corner region, at every β < 1/R, without assuming a value for u'(0). Related literature: Clarida (1987), Consumption, Liquidity Constraints and Asset Accumulation in the Presence of Random Income Fluctuations.

theorem LeanEconomics.IncomeFluctuation.minIncome_le_consumptionFn_floor {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)) (z : Z) : P.minIncome + P.interest * assetFloor ≤ P.consumptionFn z assetFloor

At the borrowing limit, nobody consumes less than the worst income. The household at the minimum is at the corner — otherwise its own Euler inequality would push it up by 1/βR.

theorem LeanEconomics.IncomeFluctuation.policy_eq_floor_of_euler {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) (z : Z) (hcond : ↑P.discount * (1 + P.interest) * du (P.minIncome + P.interest * assetFloor) < du (P.resources (a, z) - assetFloor)) : P.policy (a, z) = assetFloor

The corner from the Euler inequality. Wherever βR · u'(minIncome + r·floor) is below the marginal utility of cash on hand, the household saves nothing. The contrapositive of euler_ge, with minIncome_le_consumptionFn_floor bounding tomorrow's marginal utility.

Nothing here depends on how large β is beyond βR < 1; that is what makes it usable at β = 0.96, where the Lipschitz corner policy_eq_zero_of_corner_at is hopeless.

CRRA and log

theorem LeanEconomics.IncomeFluctuation.crra_policy_eq_zero_of_euler {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 γ) (hfl : assetFloor = 0) (hβR : ↑P.discount * (1 + P.interest) < 1) (hpos : ∀ (z : Z), ∀ x ∈ Set.Icc 0 assetCap, 0 < P.consumptionFn z x) (hslack : ∀ (z : Z), ∀ x ∈ Set.Icc 0 assetCap, P.policy (x, z) < P.maxSaving (x, z)) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) (hcond : ↑P.discount * (1 + P.interest) * P.minIncome ^ (-γ) < P.resources (a, z) ^ (-γ)) : P.policy (a, z) = 0

The Euler corner for CRRA, u' c = c ^ (-γ), at a zero borrowing limit. The test at state z is βR · minIncome^(-γ) < resources^(-γ), i.e. resources (a, z) < minIncome · (βR)^(-1/γ).