Aggregate capital is strictly positive #
Every equilibrium result so far is conditional on excess demand changing sign, and nothing in the development says that households save anything at all. This file supplies the missing economics: under log utility, households rich enough in income save strictly, and the stationary distribution then carries strictly positive aggregate capital.
Capital is the mean of the policy #
markovOp_assetCoord is the identity the whole argument runs on. The expected asset coordinate
next period is the policy today, because the asset the household carries forward does not depend
on which income shock arrives:
markovOp assetCoord = policyCoord.
With stationarity that gives aggregateCapital μ = ∫ policy dμ — aggregate capital is the mean
saving, not merely something computed from the distribution. Everything after is a lower bound
on that integral.
Rich households save, and the argument is the crudest deviation again #
Saving h rather than nothing costs u resources - u (resources - h) and gains
β (cont h - cont 0). For LOG the cost is log (m / (m - h)), which SHRINKS as resources grow,
while the gain is a fixed positive number — positive because the value function is strictly
increasing in assets, which valueFunction_lt_of_lt proves from strict monotonicity of u,
itself recovered from strict concavity. So above an explicit income level the household saves
strictly, with no envelope theorem and no Euler equation.
Since the cost falls with resources, it is enough to check the inequality at the household's
POOREST state in that income, a = 0, and it then holds at every asset level.
Reaching those households #
The income coordinate of the stationary distribution is bounded below by the worst transition
probability into that state, and that too is pure duality: the indicator of an income state is
CONTINUOUS here, Z being discrete, so it is a legitimate test function and
markovOp (incomeIndicator z₁) s = transitionMatrix s.2 z₁. Stationarity turns a uniform lower
bound on the column of the transition matrix into a lower bound on the mass.
Strict monotonicity #
Period utility is STRICTLY increasing: a concave function that is flat on an interval is affine there, which strict concavity forbids.
The value function is strictly increasing in assets. More assets buy strictly more consumption at the same saving plan.
The continuation is strictly increasing, since some income state has positive probability.
Capital is the mean of the policy #
Saving carried forward, as a bounded continuous function of the state.
Equations
Instances For
The expected asset coordinate next period is today's saving. The asset carried forward does not depend on which income shock arrives, so the expectation collapses.
Aggregate capital is mean saving.
The stationary distribution reaches every income state #
The indicator of an income state — continuous, because Z is discrete.
Equations
- P.incomeIndicator z₁ = BoundedContinuousFunction.ofNormedAddCommGroup (fun (s : P.State) => if s.2 = z₁ then 1 else 0) ⋯ 1 ⋯
Instances For
The stationary mass on an income state is at least the worst transition into it.
Rich households save #
A household with enough income saves strictly. The cost of saving h instead of nothing
is log (m / (m - h)), which falls as resources grow, while the gain β (cont h - cont 0) is a
fixed positive number. So it is enough to check the comparison at a = 0, the poorest state in
that income, and it then holds at every asset level.
The log instance of policy_pos_of_cost: the cost of saving h is log (m / (m - h)),
which falls as resources grow, so it is enough to check it at the poorest state in that income.
A uniform positive lower bound on saving across the asset region, by compactness.
Positive aggregate capital #
Aggregate capital is strictly positive. Households in income state z₁ save at least
ε, the stationary distribution puts at least p₀ of its mass there, and aggregate capital is
mean saving.
The log instance of aggregateCapital_pos_of_cost.
The gain, bounded by primitives #
policy_pos_of_income asks for a lower bound on cont z₁ h - cont z₁ 0, which is an object of
the solved model rather than a primitive. It is bounded below by the same deviation trick applied
one level down, and WHICH TERM OF THE SUM IS KEPT is the economics.
Bounding by the worst state — every income z' replaced by maxIncome — gives, for small h, a
condition amounting to β (1 + r) > 1. That is useless here: the natural asset bound wants
β (1 + r) < 1, so the two would collide. Keeping the LOW-income term instead gives
P z z₀ · log (1 + (1+r) h / income z₀), and with income z₀ small that term is large; the
condition becomes roughly β (1 + r) · P z z₀ > minIncome / maxIncome, satisfiable under ordinary
impatience provided income is dispersed.
That difference is the precautionary motive. The household saves not because it is patient but
because with probability P z z₀ it lands where consumption is small and the marginal value of
assets is large. The motive enters through the DISPERSION of income rather than through convexity
of u', which is why it is available without a third derivative.
The value of extra assets is at least the one-period utility gain, got by carrying the poorer household's own saving plan forward.
The continuation rises with saving.
A lower bound on the one-period utility gain in one successor state gives a probability-weighted lower bound on the continuation gain.
The continuation's gain between two saving levels, in primitives.
The continuation's gain from zero, in primitives. Only the term for income state z₀ is
kept; the rest are non-negative. For a LOW income z₀ the logarithm is large, and that is the
precautionary motive.
Aggregate capital is strictly positive, from primitives alone. Every hypothesis is stated
in β, r, the income levels and the transition matrix.
A quantitative lower bound on saving. A household with enough income saves at least
h/2, not merely something positive — which is what a sign change needs, since the rate at
which demand falls below supply has to be chosen from a number.
The log instance of policy_ge_of_cost.