Concavity of the consumption function as a closed class #
IncomeFluctuationConsumption showed that concavity of the consumption function cannot follow
from concavity of u and of the value function, and that it is a statement about the FIXED
POINT. This file supplies the machinery that statements about the fixed point need, and reduces
Carroll and Kimball (1996) to its single inductive step.
The pattern is the one used four times already — monotonicity, concavity, Lipschitz bounds and
increasing differences — but with one new difficulty. Those four are properties OF the value
function, closed in sup norm by isClosed_concaveOn and its relatives. Concavity of the
consumption function is a property of the value function's ARGMAX, and nothing says offhand
that an argmax survives a uniform limit. So the closure step has to be proved rather than
quoted, and that is what tendsto_policyOf does: along a uniformly convergent sequence of
continuation values the optimal actions converge, because a cluster point of the maximisers is
a maximiser of the limit and the maximiser of the limit is unique.
That gives concaveOn_consumptionFn_of_preserves: if the Bellman operator carries a concave
consumption function to a concave consumption function, the fixed point's consumption function
is concave. The iteration starts from 0, whose consumption function is resources, affine on
the asset region — policyOf_zero, an agent with no future eats everything.
What is proved, and what is left #
The hypothesis hT is the whole of Carroll and Kimball. Two thirds of it are now discharged.
The analysis. On paper the argument runs through second derivatives: risk tolerances ADD
across the optimisation, T_V(m) = T_u(c) + T_W(m - c), and Kimball's risk-tolerance
aggregation theorem propagates T_V' ≥ T_u' from the continuation to the value. PowerMean
supplies the integrated form of exactly that, with no derivative: for CRRA marginal utility the
consumption paired with a given stock of end-of-period assets is a positive multiple of the
weighted power mean, exponent -γ, of next period's consumptions, and a power mean with a
NEGATIVE exponent is concave and nondecreasing. Homogeneity turns that into the convexity of a
sublevel set, which is elementary.
The transfer. Turning concavity of that map into concavity of the consumption function is
usually done by differentiating an inverse function. concaveOn_of_egm does it from the budget
identity alone: write the choice against end-of-period assets, and the two concavities are the
same statement.
The Euler equation hEuler is proved in IncomeFluctuationEuler, and so is the step with
the BORROWING LIMIT allowed to bind. Saving more is feasible unless the household already saves
the maximum, so the inequality half of the first-order condition survives the corner; and at a
constrained state the saving is assetFloor, which lies below any average of savings, which is
the only thing concaveOn_of_egm ever needed. concaveOn_of_egm_corner and
concaveOn_consumptionFnOf_bellman are the results.
The induction's bookkeeping is done in IncomeFluctuationIterate: positivity and
monotonicity of the consumption function, proved at the fixed point in this development, restated
for an arbitrary continuation, and a uniform bound on saving that covers every iterate at once.
So Carroll and Kimball is proved -- concaveOn_consumptionFn_of_marginal for CRRA,
concaveOn_consumptionFn_of_bounded_crra for the bounded CES family 0 < γ < 1, where positive
consumption comes from the marginal Inada condition run against an arbitrary continuation.
One input is left explicit: a calibration inequality putting the asset cap above the bound on
saving. crra_policyOf_le_mul makes that bound the multiplicative one -- deviate to a FRACTION
of the saving and price the extra consumption where it lands -- so it involves the continuation's
OSCILLATION rather than its level, and the hypothesis is character for character the one
crra_policy_lt_assetCap carries. The witnesses that discharge that one discharge this one:
nearLog_concaveOn_consumptionFn is Carroll and Kimball for a concrete CES economy, at every
rate the equilibrium argument uses.
Toda's necessity result is uniform, across arbitrary return and income laws under its
regularity hypotheses with borrowing permitted; see Analysis.HARA. It does not establish that hT
is false for an individual capped household outside HARA. This file proves sufficient results
for the stated CRRA families.
OWED: this is deferred, not abandoned #
The obstruction has moved four times.
Shifted CRRA was the first sufficient utility family;
Analysis.HARAsupplies this branch.The asset cap was the second, and worse, because it made the conclusion outright FALSE --
not_concaveOn_consumptionFn_of_cap_bindsbelow.crra_policy_lt_assetCapremoves it by calibration, andnearLogis recalibrated so that saving provably never reaches the cap.Differentiability was the third, and it is now GONE:
hasDerivAt_bellmanis the Clausen and Strub sandwich run along the iteration, andPowerMeanremoves second derivatives altogether.The Euler equation was the fourth, and it is proved --
euler_eq, and without the envelope theorem at that.The borrowing-constraint kink was the fifth, and
concaveOn_of_egm_cornerabsorbs it.The induction's bookkeeping was the sixth, and
IncomeFluctuationIteratedoes it.Positive consumption for the bounded CES family was the seventh, and
positiveConsumptionAll_of_marginalInadadoes it.The cap calibration was the eighth, and
crra_policyOf_le_mulmakes it the one the witnesses already prove.
Nothing remains: nearLog_concaveOn_consumptionFn is the theorem at a concrete calibration.
This file holds the analysis and the closure step; IncomeFluctuationEuler the first-order
condition and the corner; IncomeFluctuationIterate the bookkeeping and the theorem.
Continuation values that are concave along each asset slice. This is what makes the optimal action unique, and it is preserved by the Bellman operator.
Equations
Instances For
Bellman iteration preserves concavity from any concave continuation.
The optimal action of an arbitrary continuation #
IncomeFluctuation proves uniqueness for every continuation whose asset slices are concave.
The closure argument applies that shared theorem along the whole approximating sequence; the
wrapper below gives its hypothesis the name ConcaveSlices.
The optimal action is unique for any continuation with concave slices.
The agent with no future eats everything #
The iteration starts at the zero continuation, where saving buys nothing and the optimal plan
is to consume all cash on hand. Its consumption function is resources, affine on the asset
region, so the induction has a base.
Saving more cannot raise the reward: consumption falls, and utility rises with it.
With nothing to gain from saving, the household saves nothing.
The closure step: optimal actions survive a uniform limit #
This is what the four earlier closed-class arguments got for free from isClosed_concaveOn.
Concavity of the consumption function is a property of the ARGMAX, so closure has to be proved:
a cluster point of maximisers of vₙ is a maximiser of the limit, and the maximiser of the
limit is unique.
Optimal actions survive a uniform limit.
The limit step, split off from concaveOn_consumptionFn_of_preserves: concavity of the
consumption functions of the iterates passes to the fixed point, because optimal actions survive
a uniform limit.
Carroll and Kimball, reduced to one step #
The consumption function of the fixed point is concave whenever the Bellman operator
preserves concavity of the consumption function. Everything except the hypothesis hT is
discharged: the base case, the induction, the limit.
hT is Carroll and Kimball (1996) — see the module docstring for what proving it would take.
The endogenous-gridpoint transfer #
The step that carries concavity forward is not about the Bellman operator at all. Write the
household's choice against END-OF-PERIOD assets rather than against cash on hand: let C A be
the consumption it pairs with saving A, so that the budget reads y + R a = A + C A. The
graph of the consumption function is then the curve A ↦ (A + C A, C A), and concavity of the
consumption function is exactly concavity of C.
That equivalence is elementary — it is proved below with no derivative and no inverse function,
from the budget identity and the fact that A + C A is strictly increasing. What it buys is
that the hard step moves to C, where the first-order condition makes it a POWER MEAN of next
period's consumptions, and Analysis/PowerMean settles those.
If C is nondecreasing then cash on hand is strictly increasing in end-of-period assets.
The endogenous-gridpoint transfer. With the budget written against end-of-period assets,
concavity of the consumption function is concavity of C. Derivative-free.
Carroll and Kimball for CRRA, from the first-order condition #
With CRRA marginal utility u' c = c ^ (-γ) the first-order condition says exactly that the
consumption paired with saving A is a positive multiple of the weighted power mean, exponent
-γ, of next period's consumptions at A. Analysis/PowerMean makes that map concave and
nondecreasing, and the transfer above does the rest.
The endogenous-gridpoint map for CRRA. The consumption a household with continuation v
pairs with end-of-period assets A, read off the Euler equation.
Equations
- P.egmMap v γ z A = (↑P.discount * (1 + P.interest)) ^ (-(1 / γ)) * LeanEconomics.powerMean (P.transitionMatrix z) (-γ) fun (z' : Z) => P.consumptionFnOf v z' A
Instances For
Carroll and Kimball (1996), the induction step, for CRRA. Given the Euler equation, the Bellman operator carries a concave consumption function to a concave consumption function.
Everything except hEuler is now proved: the power-mean concavity that Carroll and Kimball
obtain from Kimball's risk-tolerance aggregation, and the endogenous-gridpoint transfer that
turns it into concavity of the consumption function. hEuler is the first-order condition of
the maximisation, which holds wherever the choice is interior — see the module docstring.
The asset cap obstructs concavity, and hT is stated too strongly #
Attempting hT for log utility — the one CRRA specification this structure admits with Light's
condition, by crra_pinch — turns up an obstruction that has nothing to do with Carroll and
Kimball and everything to do with the cap.
Where the cap binds the household cannot save more, so every extra unit of resources is consumed
and the consumption function has slope exactly 1 + r. Below, wherever it saves strictly more,
the slope is strictly less. Increments therefore RISE across the kink, which concavity forbids.
not_concaveOn_consumptionFn_of_cap_binds proves it.
So hT as stated is not merely hard, it is FALSE for any calibration whose cap binds, quite
apart from the HARA question. Concavity of the consumption function on the asset region needs the
cap to be SLACK — above the natural asset bound, so that the household never wants to save that
much. That is exactly what exists_decline_of_consumption_lower_bound is about, and by
one_sub_mpc_mul_of_asymptotic the condition behind it is β (1 + r) < 1.
Which ties the two halves of the development together: the imposed assetCap, so far a
bookkeeping device for compactness, has to be justified economically before the Carroll–Kimball
hypothesis can even be true.
Once the cap binds it binds for ever after, since the policy is monotone and capped.
A binding asset cap rules out a concave consumption function.