Light (2018), step 5: increasing differences propagate across rates #
IncomeFluctuationRateMonotone reduces Theorem 1 to one hypothesis, ContIncreasingDifferences,
and records that propagating it needs two things this development did not have: the envelope
condition as an EQUALITY, and concavity of the consumption function. Both are now proved
(hasDerivAt_bellman, concaveOn_consumptionFnOf_bellman), so the step is available.
The identity the whole thing rests on #
Two rates share a budget set: cash on hand at (a, R₁) equals cash on hand at (t a, R₂) for
t = R₁ / R₂, and the saving cap is the same because it is min assetCap (cash on hand). So the
two maximisations are literally the same maximisation, and lazyValue_withRate says so. Hence
bellmanFn_withRate, policyOf_withRate and consumptionFnOf_withRate: the whole solution at
(a, R₁) is the solution at (t a, R₂).
That turns the difference (T_{R₂} f)(a) - (T_{R₁} f)(a) into (T_{R₂} f)(a) - (T_{R₂} f)(t a),
a statement about ONE economy, and increasing differences across rates becomes monotonicity of
that difference in a. The envelope makes its derivative R₂ u'(c_w(a)) - R₁ u'(c_v(t a)),
where v and w are the two continuations, and two moves sign it: single crossing in the
continuation at the scaled asset level, then mul_marginal_le_of_scale — concavity of the
consumption function for one factor, relative risk aversion at most one for the other.
Doing it in that order matters. Applying the pivotal inequality directly to c_v would need
Carroll–Kimball for economy two's choice against economy ONE's continuation, a hybrid object no
induction produces; going through c_v(t a) ≥ c_w(t a) first puts the pivotal inequality on
c_w, economy two's own, which is exactly what concaveOn_consumptionFn_of_iterates delivers.
What is left #
contIncreasingDifferences_withRate discharges the hid of policy_mono_interest, so Light's
Theorem 1 holds outright. Its hypotheses are the standing ones of this development: utility
differentiable with decreasing, non-negative marginal utility and relative risk aversion at most
one; consumption positive at every optimum; the asset cap slack along the iteration; and the
Carroll–Kimball concavity of the iterates' consumption functions. CESConcaveConsumption shows
these hold together at concrete CES calibrations.
The two rates solve the same problem at rescaled assets #
The objective at (a, r₁) is the objective at (t a, r₂), action for action.
The feasible sets coincide.
Consumption at a given action coincides.
The whole solution at (a, r₁) is the solution at (t a, r₂).
The saving chosen at (a, r₁) is the saving chosen at (t a, r₂).
Consumption too. This is the function mul_marginal_le_of_scale is applied to.
The derivative assembly #
With the budget coincidence in hand the whole comparison lives in ONE economy: the difference to be signed is
F a = (T w)(a) - (T v)(t a), t = R₁ / R₂ ≤ 1.
hasDerivAt_bellman — the Clausen–Strub lazy-agent envelope — differentiates both terms, giving
F' a = R₂ u'(c_w(a)) - t R₂ u'(c_v(t a)) = R₂ u'(c_w(a)) - R₁ u'(c_v(t a)).
The second term is signed in two moves. Single crossing in the continuation puts
c_w(t a) ≤ c_v(t a), so u'(c_v(t a)) ≤ u'(c_w(t a)); and then mul_marginal_le_of_scale,
Light's pivotal inequality, carries R₁ u'(c_w(t a)) ≤ R₂ u'(c_w(a)). Note which consumption
function the pivotal inequality is applied to: c_w, economy TWO's own, whose concavity is what
Carroll–Kimball delivers. Routing the comparison through c_w rather than through c_v is what
keeps the argument inside one economy's Carroll–Kimball theorem — c_v is the hybrid object
(economy two's choice against economy one's continuation) and no concavity of it is needed.
Note what the envelope is asked for: the state interior and the CHOICE strictly below the saving cap. Nothing is asked at the borrowing constraint, so the argument survives where it binds.
The monotone difference, in one economy, from the pivotal inequality as a hypothesis. If
t ≤ 1, the continuations v and w have increasing differences, and t R u'(c_w(t a)) ≤ R u'(c_w(a)) at every interior a, then a ↦ (T w)(a) - (T v)(t a) is nondecreasing.
The monotone difference, in one economy. If t ≤ 1 and the continuations v and w have
increasing differences, then a ↦ (T w)(a) - (T v)(t a) is nondecreasing. The pivotal inequality
is supplied by mul_marginal_le_of_scale: relative risk aversion at most one and a concave,
increasing consumption function.
The step, across rates #
Reading the difference back through the budget coincidence turns the previous theorem into the statement Light's induction propagates: the Bellman images of two continuations with increasing differences again have increasing differences, at the two rates.
Light (2018), step 5, from the pivotal inequality as a hypothesis.
Light (2018) Theorem 1 from the pivotal inequality, the induction started anywhere.
Light (2018), step 5. Increasing differences survive the Bellman operator.
The induction, and the limit #
IncDiffSlices mentions no economy and is closed under pointwise limits, so the step iterates
from the common start 0 and passes to the two value functions. That discharges the hypothesis
hid of policy_mono_interest, and with it Light's Theorem 1.
Light (2018) Theorem 1, with step 5 discharged. The value functions at two rates have increasing differences in assets, so the continuations do.
Light (2018) Theorem 1, unconditional on the increasing-differences hypothesis. A household facing a higher interest rate saves at least as much, at every asset level and every income state.
CRRA, with the marginal-utility hypotheses discharged #
For u = crraUtility γ marginal utility is c ^ (-γ), which is decreasing and non-negative for
every γ > 0, and c · u'(c) = c ^ (1 - γ) is nondecreasing exactly when γ ≤ 1 — relative
risk aversion at most one, the hypothesis Light needs and the one this development has carried
since RelativeRiskAversion.
Beyond relative risk aversion one #
The relative-risk-aversion specializations use γ ≤ 1 in one place: the pivotal inequality
t R u'(c_w(t a)) ≤ R u'(c_w(a)) applied to economy two's consumption function against the
CURRENT continuation w. Two changes make that inequality a hypothesis one can hope to meet
when γ > 1.
First, run the induction from economy two's own value function rather than from 0. The
economy-two iterates are then constant — T₂ V₂ = V₂ — so the pivotal inequality is asked of
economy two's TRUE consumption function alone, not of every iterate (whose consumption functions
start at "eat everything", where no such inequality holds).
Second, mul_rpow_neg_le_of_scale gives the inequality for u' = c^{-γ}, any γ, wherever
(1 - c₂(0)/c₂(t a))(ρ - 1) ≤ ρ^{1/γ} - 1 with ρ = R₂/R₁ — a condition on the range of the
consumption function, roughly c₂(a) ≤ (γ/(γ-1)) c₂(0) for rates close together. It is a
restriction on wealth, not on preferences: for a small enough asset cap, or on an invariant
interval, Light's Theorem 1 holds for every γ.
Light (2018) Theorem 1 from the pivotal inequality on economy two's OWN consumption function. The induction is started at economy two's value function, which its Bellman operator fixes, so the only consumption function the inequality is asked of is the true one at the higher rate.
Light (2018) Theorem 1 for CRRA with ANY γ > 0, on a range condition. Saving rises with
the rate at every state provided economy two's consumption function satisfies
(1 - c₂(0,z)/c₂(t a, z)) (ρ - 1) ≤ ρ^{1/γ} - 1 for ρ = R₂/R₁, t = 1/ρ, at every interior
a — for rates close together, consumption at most about γ/(γ-1) times its value at zero
assets. Concavity of that consumption function is Carroll--Kimball at the fixed point
(concaveOn_consumptionFn_of_crra).