Carroll and Kimball beyond CRRA: the HARA induction step #
IncomeFluctuationCarrollKimball proves the induction step for u = crraUtility γ, where the
Euler equation makes consumption a multiple of the power mean of next period's consumptions and
powerMean_concave — Kimball's risk-tolerance aggregation — does the rest. Carroll and Kimball's
theorem is not about CRRA but about HARA, and this file covers the b ≠ 0 branch,
u c = crraUtility γ (η + c): CRRA with a subsistence level, which includes CRRA itself at
η = 0.
Nothing new is needed #
Marginal utility is (η + c) ^ (-γ), so the Euler equation reads
(η + C(A)) ^ (-γ) = β R · Σ_{z'} π_{z z'} (η + c_{z'}(A)) ^ (-γ),
which is the CRRA equation in the variable η + c. So the endogenous-gridpoint map is the CRRA
one applied to SHIFTED consumptions, with the shift removed at the end (haraEgmMap), and it is
concave for exactly the same reason: η + c_{z'} is concave when c_{z'} is, the power mean of
concave positive functions is concave, and a constant shift changes nothing.
That the shift is harmless is the content of "linear risk tolerance". Risk tolerance
-u' / u'' is (η + c) / γ, affine in consumption, and Kimball's aggregation theorem needs
precisely affineness — the level η rides through untouched.
What is and is not covered #
The induction STEP is here, for the whole b ≠ 0 HARA branch. What is not is the assembled
statement: the iteration also needs positive consumption and the asset cap slack. Those are no
longer CRRA-specific — consumptionFnOf_pos_of_marginal gets positivity from a FINITE marginal
bound, which is what a shifted CRRA has at zero ((η + c) ^ (-γ) at c = 0 is η ^ (-γ)), and
policyOf_le_of_marginal_bound was always general. Both branches now carry the assembly
through to a witness: IncomeFluctuationCARA.caraCal for CARA, and StoneGearyWitness.stoneGeary
for this one. The CARA branch b = 0, where marginal utility is exp (-α c), needs a
different aggregator — the soft minimum -(1/α) log Σ π exp (-α c) — and is in
IncomeFluctuationCARA, on top of Analysis.SoftMin.
The endogenous-gridpoint map for shifted CRRA. The CRRA map in the variable η + c.
Equations
- P.haraEgmMap v γ η z A = ((↑P.discount * (1 + P.interest)) ^ (-(1 / γ)) * LeanEconomics.powerMean (P.transitionMatrix z) (-γ) fun (z' : Z) => η + P.consumptionFnOf v z' A) - η
Instances For
The Euler equation puts consumption on the endogenous grid, for shifted CRRA.
The Euler hypothesis discharged, for shifted CRRA: interiority is all that is left.
Carroll and Kimball (1996), the induction step for shifted CRRA. Given the Euler equation, the Bellman operator carries a concave consumption function to a concave one.
The induction step for shifted CRRA, with the Euler equation proved, exactly as
concaveOn_consumptionFnOf_bellman_of_interior does it for CRRA: what is assumed is interiority,
a property of the state, not of the model.
CRRA is the η = 0 member, so the HARA step really does generalise the CRRA one rather
than sitting beside it.
Marginal bounds #
A shifted CRRA has FINITE marginal utility at zero, η ^ (-γ), so like CARA it satisfies no
Inada condition and its consumption floor is an inequality rather than a limit. Both bounds are
the CRRA ones read at η + c.
The same with the restriction moved from γ to the ARGUMENT: a strictly positive
subsistence level keeps η + c away from zero, so γ ≥ 1 — log Stone–Geary included — is
admissible.
A marginal bound near zero for a strictly positive subsistence level.
The Euler inequality, and the corner #
The Euler INEQUALITY in endogenous-gridpoint form, for shifted CRRA: it holds AT the borrowing limit, where the equality fails.
Carroll and Kimball for shifted CRRA, across the borrowing-limit kink.
The proportional bound on saving #
policyOf_le_of_marginal_bound prices a deviation against the LEVEL of the continuation, which
for a bounded utility is far too crude to keep the cap slack at any interesting discount factor.
The CRRA development fixes that with crra_policyOf_le_mul: deviate to a FRACTION θ of the
saving rather than a fixed amount, and price the extra consumption at the margin where it lands.
The bound then involves the continuation's OSCILLATION and is proportional to consumption.
The shifted-CRRA version is that argument with the marginal step read at η + c. Everything
else — the deviation, the concavity of the continuation, the oscillation — knows nothing about
preferences.
Saving never reaches the asset cap, for shifted CRRA.
The assembly #
Carroll and Kimball for shifted CRRA, from two inequalities. The same two the CARA assembly needs, and for the same reasons: marginal utility at zero is finite, so the consumption floor has to be earned, and the cap has to sit above the saving the marginal bound allows.
The two comparative-statics corollaries, for shifted CRRA #
Light's Theorem 1 and the impatience-driven decline both take the marginal-utility hypotheses
abstractly, so shifted CRRA discharges them the same way CRRA does — with (η + c) ^ (-γ) in
place of c ^ (-γ). Relative risk aversion of the shifted family is γc/(η + c) ≤ γ, so a
NON-NEGATIVE subsistence level only helps Light's condition.
Light (2018) Theorem 1 for shifted CRRA.
Worst-state decline for shifted CRRA: the decline condition is impatience.
The supply floor #
The household saves something, so aggregate capital is positive. The shape is the CRRA one: the
cost of saving a little is priced at the margin where consumption is lowest, the gain at the
margin in the bad successor state, and the comparison is between two marginal utilities. With a
subsistence level both are read at η + c.
The continuation's gain, for shifted CRRA.
Saving is bounded below, for shifted CRRA, when the gain beats the cost.
The corner condition, in primitives #
The corner test of policy_eq_zero_of_corner_at is β L < m: the discounted slope of the value
function against the marginal value of consumption. Both sides have closed forms for shifted
CRRA, so the test becomes one inequality among the primitives.
- The value function's slope is bounded by
slopeBoundU, amplified by the return and the discounting. Concavity pricesslopeBoundUat the margin halfway down the minimum consumption:(η + minConsumption / 2) ^ (-γ). - The marginal value at
(a, z₀)fora ≤ a₀is at least(η + income z₀ + R a₀) ^ (-γ).
A sufficient condition for the corner to hold below a₀ is
β · (η + minConsumption/2) ^ (-γ) · R / (1 - β R) < (η + income z₀ + R a₀) ^ (-γ),
which is checkable by norm_num at any calibration.
The slope constant in closed form.
The Lipschitz constant of the value function, in primitives.
Equations
Instances For
The value function is Lipschitz, with the constant read off the primitives.
The corner condition from primitives. One inequality, norm_num-checkable.
Positive aggregate capital for shifted CRRA, from primitives.
The supply floor with the two powers bounded separately. The gain condition compares
(η + y₁ - t)^(-γ), the marginal cost of saving t in the high state, against
(η + y₀ + Rt)^(-γ), the marginal value of having it in the low state. Bounding the first from
above and the second from below leaves ONE inequality among the bounds — and when a base sits on
the right side of one, its bound needs no root at all (rpow_neg_le_one_of_one_le,
rpow_neg_le_inv_of_le_one).
This is what makes a supply floor a calibration check rather than a proof.