The lazy agent's value, and the envelope condition

Clausen and Strub's construction: to show the value function is differentiable in assets, exhibit a differentiable LOWER bound touching it. Freeze the optimal saving and vary the state — the "lazy" agent, who meets an unfamiliar state by making the choice that was optimal at a familiar one.

The point is structural. Once the saving is frozen, current assets enter the objective ONLY through the reward, because the continuation value depends on the saving chosen and on the current income state, never on current assets. So the lazy value is u composed with an affine map plus a constant, and is differentiable wherever u is.

Concavity of the value function, already proved, then supplies the upper half of the sandwich via ConcaveOn.hasDerivAt_of_lowerBound, and the derivative is the envelope condition

V'(a) = (1 + r) · u'(c),

which is the expression Light (2018) Theorem 1 is built on.

noncomputable def LeanEconomics.IncomeFluctuation.lazyValue {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) (a' a : ℝ) : ℝ

The lazy agent's value. The saving a' is frozen; only current assets vary.

Equations

• P.lazyValue v z a' a = P.u (P.resources (a, z) - a') + ↑P.discount * ∑ z' : Z, P.transitionMatrix z z' * v (a', z')

theorem LeanEconomics.IncomeFluctuation.hasDerivAt_resources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z : Z} {a : ℝ} (ha : assetFloor < a) : HasDerivAt (fun (x : ℝ) => P.resources (x, z)) (1 + P.interest) a

Resources are affine in assets above the borrowing constraint.

theorem LeanEconomics.IncomeFluctuation.hasDerivAt_lazyValue {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) (a' : ℝ) {a du : ℝ} (ha : assetFloor < a) (hu : HasDerivAt P.u du (P.resources (a, z) - a')) : HasDerivAt (P.lazyValue v z a') ((1 + P.interest) * du) a

The lazy value is differentiable, because current assets enter only through the reward once the saving is frozen.

theorem LeanEconomics.IncomeFluctuation.lazyValue_le_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) {a' a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hmem : a' ∈ P.toExtended.feasible (a, z)) (hc : P.consumption (a, z) a' ∈ P.dom) : P.lazyValue v z a' a ≤ P.toExtended.bellmanFn v (a, z)

The lazy value is a lower bound: freezing a feasible saving can only do worse than optimising. Stated on the utility DOMAIN, so that it survives the bounded family, where zero consumption is admissible and positivity has to be earned.

theorem LeanEconomics.IncomeFluctuation.lazyValue_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) {a' a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hmem : a' ∈ P.toExtended.feasible (a, z)) (hc : 0 < P.consumption (a, z) a') : P.lazyValue v z a' a ≤ P.toExtended.bellmanFn v (a, z)

theorem LeanEconomics.IncomeFluctuation.lazyValue_eq_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) {a' a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hmem : a' ∈ P.toExtended.feasible (a, z)) (hc : P.consumption (a, z) a' ∈ P.dom) (hopt : P.toExtended.objectiveE v (a, z) a' = ↑(P.toExtended.bellmanFn v (a, z))) : P.lazyValue v z a' a = P.toExtended.bellmanFn v (a, z)

At the optimum the lazy value touches the Bellman value.

theorem LeanEconomics.IncomeFluctuation.lazyValue_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (z : Z) {a' a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hmem : a' ∈ P.toExtended.feasible (a, z)) (hc : 0 < P.consumption (a, z) a') (hopt : P.toExtended.objectiveE v (a, z) a' = ↑(P.toExtended.bellmanFn v (a, z))) : P.lazyValue v z a' a = P.toExtended.bellmanFn v (a, z)

The envelope theorem

Concavity supplies the upper half of the sandwich, the lazy agent the lower half. The only work is the neighbourhood: the frozen saving is feasible at the state it came from, but at poorer states it need not be, so the lower bound is only local. Continuity of the feasible boundary gives an interval on which it survives, provided the saving is interior there.

theorem LeanEconomics.IncomeFluctuation.hasDerivAt_bellman_of_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {z : Z} {a a' du : ℝ} (ha : assetFloor < a) (hacap : a < assetCap) (hconc : ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (x : ℝ) => (P.toExtended.bellman v) (x, z)) (ha'mem : a' ∈ P.toExtended.feasible (a, z)) (hopt : P.toExtended.objectiveE v (a, z) a' = ↑(P.toExtended.bellmanFn v (a, z))) (hint : a' < P.maxSaving (a, z)) (hc : 0 < P.consumption (a, z) a') (hu : HasDerivAt P.u du (P.consumption (a, z) a')) : HasDerivAt (fun (x : ℝ) => (P.toExtended.bellman v) (x, z)) ((1 + P.interest) * du) a

The envelope condition for bellman v. The marginal value of assets is the gross interest rate times the marginal utility of the consumption the household actually chooses. Clausen and Strub's sandwich, run one step of the iteration at a time rather than at the fixed point.

theorem LeanEconomics.IncomeFluctuation.hasDerivAt_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hpc : P.PositiveConsumption) {z : Z} {a du : ℝ} (ha : assetFloor < a) (hacap : a < assetCap) (hint : P.policy (a, z) < P.maxSaving (a, z)) (hu : HasDerivAt P.u du (P.resources (a, z) - P.policy (a, z))) : HasDerivAt (fun (x : ℝ) => P.toExtended.valueFunction (x, z)) ((1 + P.interest) * du) a

At the borrowing constraint

The sandwich does NOT extend to the left endpoint, and the failure is not technical. Its first step is that U - L has a local minimum where the bounds touch, forcing the two derivatives to agree; at an endpoint a minimum gives only d' ≥ 0, so the upper bound may be strictly steeper and the derivative is not pinned.

The right-derivative at the constraint is instead obtained as a LIMIT of the interior derivatives, using that a derivative extends continuously to an endpoint (hasDerivWithinAt_Ici_of_tendsto_deriv). This matters because a = 0 is precisely the atom the whole ergodic argument runs on, so a statement that stops short of it would stop short of the states that carry the stationary distribution.

theorem LeanEconomics.IncomeFluctuation.hasDerivWithinAt_valueFunction_Ici {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {z : Z} {g : ℝ → ℝ} {e b : ℝ} (hb : 0 < b) (hderiv : ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun (y : ℝ) => P.toExtended.valueFunction (y, z)) (g x) x) (hlim : Filter.Tendsto g (nhdsWithin 0 (Set.Ioi 0)) (nhds e)) : HasDerivWithinAt (fun (y : ℝ) => P.toExtended.valueFunction (y, z)) e (Set.Ici 0) 0