Light (2018) Theorem 1: saving rises with the interest rate

Numbered Light references use the October 31, 2018 author draft, printed page 13: https://www.researchgate.net/publication/314238962

This is the last link in the uniqueness chain. CapitalSupplyMonotone turns a uniformly larger policy into larger aggregate capital (Theorem 2), and Equilibrium.Uniqueness turns monotone capital supply into a unique equilibrium rate (Theorem 3). What is still needed is that the policy IS uniformly larger at the higher rate, which is Theorem 1.

The comparison is at a rescaled asset level

Light's device is that two problems at different rates share a budget set. Cash on hand at (a, R₁) is y + R₁ a, and at (t a, R₂) with t = R₁ / R₂ it is y + R₂ t a = y + R₁ a — the same. The saving cap is the same too, being min assetCap (cash on hand). So the two maximisations run over the SAME interval with the SAME current-consumption map, and differ only in the continuation.

That reduces the comparison to single crossing, and single crossing here is derivative-free. policy_le_of_cont_increasingDifferences is the exchange argument of policy_mono run in the other direction: there, one objective at two states; here, two objectives at one state. The hypothesis is that the continuation has INCREASING DIFFERENCES across the two rates — the integrated form of Light's f'(·, R₂) ≥ f'(·, R₁), needing no derivative and closed under pointwise limits.

The theorem then chains

g(a, R₁) ≤ g(t a, R₂) ≤ g(a, R₂),

the first step single crossing and the second policy_mono, since t ≤ 1.

The hypothesis hid, and where it is discharged

The hypothesis hid is the property Light propagates through the operator, and propagating it is his step 5. That step is not derivative-free and cannot be made so: it runs on the envelope condition (Tf)'(a, R) = R u'(σ_f(a, R)) as an EQUALITY, and the derivative-free substitute is a sandwich between two utility increments which is strictly loose. The Clausen–Strub lemma in Analysis.DifferentiableSandwich is exactly the statement that the sandwich closes only in the derivative limit.

It is now PROVED, in IncomeFluctuationRateStep: contIncreasingDifferences_withRate. The envelope equality it needs is hasDerivAt_bellman, Clausen–Strub's lazy agent, and the other input is the Carroll–Kimball concavity of the consumption function. Theorem 1 with hid discharged is policy_mono_withRate'.

Worth recording precisely: his step 5 applies Lemma 4 to σ_f(·, R₂) and needs it CONCAVE. That is Light's Lemma 5, which is the Carroll and Kimball theorem — the hypothesis hT of IncomeFluctuationCarrollKimball. So the residual hypothesis here and the residual hypothesis there are not two gaps but one: concavity of the consumption function. Closing it closes both. Toda's necessity result concerns concavity uniformly across return and income laws under its regularity hypotheses with borrowing permitted. It does not exclude concavity outside HARA for this capped model; see Analysis.HARA for the source.

The pivotal inequality that step 5 turns on, mul_marginal_le_of_scale, is already proved.

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

Increasing differences of the continuation across two rates: the integrated form of Light's f'(·, R₂) ≥ f'(·, R₁). No derivative, and closed under pointwise limits.

Equations

• P.ContIncreasingDifferences Q = ∀ (z : Z) (x y : ℝ), x ∈ Set.Icc 0 assetCap → y ∈ Set.Icc 0 assetCap → x ≤ y → P.cont z y - P.cont z x ≤ Q.cont z y - Q.cont z x

theorem LeanEconomics.IncomeFluctuation.contIncreasingDifferences_of_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hP : P.transitionMatrix = Q.transitionMatrix) (hv : ∀ (z : Z) (x y : ℝ), x ∈ Set.Icc 0 assetCap → y ∈ Set.Icc 0 assetCap → x ≤ y → P.toExtended.valueFunction (y, z) - P.toExtended.valueFunction (x, z) ≤ Q.toExtended.valueFunction (y, z) - Q.toExtended.valueFunction (x, z)) : P.ContIncreasingDifferences Q

It suffices to have increasing differences slice by slice in the value function, when the two economies share an income process.

theorem LeanEconomics.IncomeFluctuation.policy_le_of_cont_increasingDifferences {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hu : P.u = Q.u) (hdom : P.dom = Q.dom) (hβ : ↑P.discount = ↑Q.discount) (hid : P.ContIncreasingDifferences Q) {a₁ a₂ : ℝ} {z : Z} (h₁ : a₁ ∈ Set.Icc 0 assetCap) (h₂ : a₂ ∈ Set.Icc 0 assetCap) (hres : P.resources (a₁, z) = Q.resources (a₂, z)) : P.policy (a₁, z) ≤ Q.policy (a₂, z)

Single crossing across rates. Two problems whose budget sets coincide and which differ only in the continuation are ordered by the continuation: increasing differences make the second save at least as much.

This is the exchange argument of policy_mono, turned round — there one objective at two states, here two objectives at one state.

The rescaled asset level

noncomputable def LeanEconomics.IncomeFluctuation.rateScale {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) : ℝ

The asset level at the higher rate that gives the same cash on hand.

Equations

• P.rateScale Q = (1 + P.interest) / (1 + Q.interest)

theorem LeanEconomics.IncomeFluctuation.rateScale_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) : 0 < P.rateScale Q

theorem LeanEconomics.IncomeFluctuation.rateScale_le_one {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hr : P.interest ≤ Q.interest) : P.rateScale Q ≤ 1

theorem LeanEconomics.IncomeFluctuation.resources_rateScale {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hinc : P.income = Q.income) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.resources (a, z) = Q.resources (P.rateScale Q * a, z)

theorem LeanEconomics.IncomeFluctuation.rateScale_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hr : P.interest ≤ Q.interest) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) : P.rateScale Q * a ∈ Set.Icc 0 assetCap

Theorem 1

theorem LeanEconomics.IncomeFluctuation.policy_mono_interest {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P Q : IncomeFluctuation Z 0 assetCap) (hu : P.u = Q.u) (hdom : P.dom = Q.dom) (hβ : ↑P.discount = ↑Q.discount) (hinc : P.income = Q.income) (hr : P.interest ≤ Q.interest) (hid : P.ContIncreasingDifferences Q) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) ≤ Q.policy (a, z)

Light (2018) Theorem 1. A household facing a higher interest rate saves at least as much, at every asset level and every income state.

The hypothesis hid is Light's step 5; it is discharged in IncomeFluctuationRateStep by contIncreasingDifferences_withRate, which needs the envelope condition together with concavity of the consumption function. See policy_mono_withRate' for the form without it.

theorem LeanEconomics.IncomeFluctuation.policy_mono_withRate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {r₁ r₂ : ℝ} (h₁ : P.RateOK r₁) (h₂ : P.RateOK r₂) (hr : r₁ ≤ r₂) (hid : (P.withRate r₁ h₁).ContIncreasingDifferences (P.withRate r₂ h₂)) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : (P.withRate r₁ h₁).policy (a, z) ≤ (P.withRate r₂ h₂).policy (a, z)

Theorem 1 for a rate family, in the form CapitalSupplyMonotone consumes: the policy of P.withRate r rises with r.