Light's Theorem 1 at large β

policy_mono_withRate_hara — a household facing a higher rate saves at least as much — needs the saving cap slack along BOTH iterations, and in particular for the higher-rate economy choosing against the lower-rate economy's iterates. Calibrated supplies that from an oscillation bound uniform in the rate, which at Aiyagari's β = 0.96 is off by orders of magnitude.

This file supplies it from the minimal MPC instead, and the price is that the two rates have to be CLOSE: within 1 - Þ₁ of each other, where Þ₁ = (βR₁)^(1/γ) is the patience factor at the lower rate. That is not a defect of the estimate but of the comparison — a household facing a much higher rate against an old continuation can save more than its own cap — and it costs nothing, because monotonicity on overlapping short intervals is monotonicity on their union (monotoneOn_of_local).

The hybrid bound

Economy 2 choosing against economy 1's iterate v at assets a is economy 1 choosing against v at t a, t = R₁/R₂ ≤ 1 (consumptionFnOf_withRate). Consumption rises with assets, so economy 2's consumption at a is at least economy 1's at a itself, which the minimal MPC bounds by κ₁ (y + R₁ a). Saving is then at most (1-κ₁) y + (R₂ - κ₁ R₁) a, and R₂ - κ₁ R₁ = Þ₁ + (r₂ - r₁): the coefficient on assets exceeds Þ₁ by exactly the rate gap.

Local monotonicity is monotonicity

theorem LeanEconomics.monotoneOn_of_local {f : ℝ → ℝ} {lo hi ε : ℝ} (hε : 0 < ε) (h : ∀ x ∈ Set.Icc lo hi, ∀ y ∈ Set.Icc lo hi, x ≤ y → y - x ≤ ε → f x ≤ f y) : MonotoneOn f (Set.Icc lo hi)

Monotone on short steps, monotone on the interval. If f x ≤ f y whenever x ≤ y are at most ε apart, then f is monotone on the interval: walk from x to y in steps of ε.

theorem LeanEconomics.IncomeFluctuation.concaveSlices_iterate_zero {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (n : ℕ) : ConcaveSlices assetFloor assetCap (P.toExtended.bellman^[n] 0)

Every iterate from 0 has concave slices.

The hybrid cap slack

theorem LeanEconomics.IncomeFluctuation.crra_policyOf_withRate_lt_cap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) {r₁ r₂ : ℝ} (h₁ : P.RateOK r₁) (h₂ : P.RateOK r₂) (hr : r₁ ≤ r₂) (hκ₁ : 0 < (P.withRate r₁ h₁).minMPC γ) (hβ : 0 < ↑P.discount) (hpos₁ : ∀ (n : ℕ) (z : Z), ∀ a ∈ Set.Icc 0 assetCap, 0 < (P.withRate r₁ h₁).consumptionFnOf ((P.withRate r₁ h₁).toExtended.bellman^[n] 0) z a) (hthr₁ : (1 - (P.withRate r₁ h₁).minMPC γ) * (P.maxIncome + (1 + r₁) * assetCap) < assetCap) (hgap : (1 - (P.withRate r₁ h₁).minMPC γ) * P.maxIncome + ((1 - (P.withRate r₁ h₁).minMPC γ) * (1 + r₁) + (r₂ - r₁)) * assetCap < assetCap) (n : ℕ) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : (P.withRate r₂ h₂).policyOf ((P.withRate r₁ h₁).toExtended.bellman^[n] 0) (a, z) < assetCap

Cap slack for the higher-rate economy against the lower-rate economy's iterates, from the minimal MPC at the lower rate. The condition is one inequality in which the rate gap appears explicitly.

Light's Theorem 1, locally

theorem LeanEconomics.IncomeFluctuation.crra_policy_mono_withRate_of_minMPC {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ ≤ 1) (hu : P.u = crraUtility γ) {r₁ r₂ : ℝ} (h₁ : P.RateOK r₁) (h₂ : P.RateOK r₂) (hr : r₁ ≤ r₂) (hκ₁ : 0 < (P.withRate r₁ h₁).minMPC γ) (hκ₂ : 0 < (P.withRate r₂ h₂).minMPC γ) (hβ : 0 < ↑P.discount) (hpc₁ : (P.withRate r₁ h₁).PositiveConsumptionAll) (hpc₂ : (P.withRate r₂ h₂).PositiveConsumptionAll) (hthr₁ : (1 - (P.withRate r₁ h₁).minMPC γ) * (P.maxIncome + (1 + r₁) * assetCap) < assetCap) (hthr₂ : (1 - (P.withRate r₂ h₂).minMPC γ) * (P.maxIncome + (1 + r₂) * assetCap) < assetCap) (hgap : (1 - (P.withRate r₁ h₁).minMPC γ) * P.maxIncome + ((1 - (P.withRate r₁ h₁).minMPC γ) * (1 + r₁) + (r₂ - r₁)) * assetCap < assetCap) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : (P.withRate r₁ h₁).policy (a, z) ≤ (P.withRate r₂ h₂).policy (a, z)

A household facing a slightly higher rate saves at least as much, for CRRA with γ ≤ 1, with every cap-slack hypothesis discharged from the minimal MPC. Positivity against arbitrary concave continuations is the one hypothesis left, and it is free for CRRA (Inada).