The Bellman operator preserves Lipschitz continuity in assets

The economics half of the Lipschitz argument. With isClosed_forall_lipschitzOn this makes the value function Lipschitz in assets, which bounds the marginal value of wealth uniformly and so lets a corner condition be checked without differentiating anything.

The action swap

Comparing a richer state x with a poorer state y ≤ x, the resource shortfall is Δ = (1+r)(x-y). Given any action a' feasible at x, the action max 0 (a' - Δ) is feasible at y and — away from the truncation — leaves consumption EXACTLY unchanged. So the whole difference passes to the continuation value, where the hypothesis on v bounds it by L·Δ, and the utility term contributes nothing.

Where the truncation bites, the poorer household saves nothing and therefore consumes all its resources. That is what keeps the utility term controllable: both consumptions are then at least minIncome, where a concave u is Lipschitz with the explicit constant of slopeBound. No appeal to the cutoff lemma is needed, and no derivative.

Those two cases are where the constant (K + βL)(1+r) comes from, and solving (K + βL)(1+r) ≤ L for L is exactly where impatience β(1+r) < 1 is required.

noncomputable def LeanEconomics.IncomeFluctuation.slopeBoundU {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ℝ

The Lipschitz constant of u above the lowest possible consumption.

Equations

• P.slopeBoundU = slopeBound P.u P.minConsumption

theorem LeanEconomics.IncomeFluctuation.slopeBoundU_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : 0 ≤ P.slopeBoundU

theorem LeanEconomics.IncomeFluctuation.abs_u_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {c d : ℝ} (hc : P.minConsumption ≤ c) (hd : P.minConsumption ≤ d) : |P.u c - P.u d| ≤ P.slopeBoundU * |c - d|

theorem LeanEconomics.IncomeFluctuation.abs_expect_sub_le_lipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {L : ℝ} (hv : ∀ (z : Z), ∀ p ∈ Set.Icc assetFloor assetCap, ∀ q ∈ Set.Icc assetFloor assetCap, |v (p, z) - v (q, z)| ≤ L * |p - q|) (z : Z) {a b : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hb : b ∈ Set.Icc assetFloor assetCap) (x y : ℝ) : |P.toExtended.expect v ((x, z), a) - P.toExtended.expect v ((y, z), b)| ≤ L * |a - b|

The expectation inherits a Lipschitz bound from the continuation value, since the two states share the income draw and hence the transition weights.

theorem LeanEconomics.IncomeFluctuation.bellmanFn_sub_le_of_lipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {L : ℝ} (hL : 0 ≤ L) (hv : ∀ (z : Z), ∀ p ∈ Set.Icc assetFloor assetCap, ∀ q ∈ Set.Icc assetFloor assetCap, |v (p, z) - v (q, z)| ≤ L * |p - q|) (z : Z) {x y : ℝ} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) (hxy : y ≤ x) : P.toExtended.bellmanFn v (x, z) - P.toExtended.bellmanFn v (y, z) ≤ (P.slopeBoundU + ↑P.discount * L) * ((1 + P.interest) * (x - y))

The richer state's value exceeds the poorer's by at most the swap cost.

theorem LeanEconomics.IncomeFluctuation.bellmanFn_sub_le_of_lipschitz' {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {L : ℝ} (hL : 0 ≤ L) (hv : ∀ (z : Z), ∀ p ∈ Set.Icc assetFloor assetCap, ∀ q ∈ Set.Icc assetFloor assetCap, |v (p, z) - v (q, z)| ≤ L * |p - q|) (z : Z) {x y : ℝ} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) (hxy : y ≤ x) : P.toExtended.bellmanFn v (y, z) - P.toExtended.bellmanFn v (x, z) ≤ ↑P.discount * L * ((1 + P.interest) * (x - y))

The poorer state's value falls short by at most the swap cost. The reverse swap needs no utility bound at all: where it truncates, the richer household consumes strictly more, so the utility term has the helpful sign.

theorem LeanEconomics.IncomeFluctuation.abs_bellmanFn_sub_le_of_lipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {L : ℝ} (hL : 0 ≤ L) (hv : ∀ (z : Z), ∀ p ∈ Set.Icc assetFloor assetCap, ∀ q ∈ Set.Icc assetFloor assetCap, |v (p, z) - v (q, z)| ≤ L * |p - q|) (hbig : (P.slopeBoundU + ↑P.discount * L) * (1 + P.interest) ≤ L) (z : Z) {x y : ℝ} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) : |P.toExtended.bellmanFn v (x, z) - P.toExtended.bellmanFn v (y, z)| ≤ L * |x - y|

The Bellman operator preserves Lipschitz continuity in assets.

theorem LeanEconomics.IncomeFluctuation.valueFunction_lipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {L : ℝ} (hL : 0 ≤ L) (hbig : (P.slopeBoundU + ↑P.discount * L) * (1 + P.interest) ≤ L) (z : Z) (x : ℝ) : x ∈ Set.Icc assetFloor assetCap → ∀ y ∈ Set.Icc assetFloor assetCap, |P.toExtended.valueFunction (x, z) - P.toExtended.valueFunction (y, z)| ≤ L * |x - y|

The value function is Lipschitz in assets, with an explicit constant. Combining the preservation proof with the closed class. Any L with (K + βL)(1+r) ≤ L works, and such an L exists exactly when β(1+r) < 1.

The corner

With the marginal value of wealth bounded above by L, saving nothing beats saving anything as soon as β L falls below a lower bound on the marginal utility of consumption. Both sides of that comparison are now explicit constants, and no derivative appears in either.

theorem LeanEconomics.IncomeFluctuation.policy_eq_zero_of_corner_at {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {L m : ℝ} (hlip : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, ∀ y ∈ Set.Icc assetFloor assetCap, |P.toExtended.valueFunction (x, z) - P.toExtended.valueFunction (y, z)| ≤ L * |x - y|) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (hmarg : ∀ (c d : ℝ), d ∈ P.dom → d ≤ c → c ≤ P.resources s - assetFloor → m * (c - d) ≤ P.u c - P.u d) (hcond : ↑P.discount * L < m) : P.policy s = assetFloor

The corner condition, state by state. The marginal-utility bound is required only up to THIS state's resources, so the threshold is local: a state with few resources has high marginal utility and the constraint binds there, while a richer state may fail the test.

That is what lets the borrowing constraint bind at a bad income draw without binding everywhere, which the global version could not express.

theorem LeanEconomics.IncomeFluctuation.policy_eq_zero_of_corner {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {L m : ℝ} (hlip : ∀ (z : Z), ∀ x ∈ Set.Icc assetFloor assetCap, ∀ y ∈ Set.Icc assetFloor assetCap, |P.toExtended.valueFunction (x, z) - P.toExtended.valueFunction (y, z)| ≤ L * |x - y|) (hmarg : ∀ (c d : ℝ), d ∈ P.dom → d ≤ c → c ≤ P.maxConsumption → m * (c - d) ≤ P.u c - P.u d) (hcond : ↑P.discount * L < m) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : P.policy s = assetFloor

The global corner condition, as a corollary.

theorem LeanEconomics.IncomeFluctuation.crra_marginal {R : ℝ} (hR : 0 < R) (c d : ℝ) (hd : 0 < d) (hdc : d ≤ c) (hcR : c ≤ R) : 1 / R ^ 2 * (c - d) ≤ -c⁻¹ - -d⁻¹

For u c = -1/c, the marginal-utility bound up to R is 1/R². So the state-dependent threshold reads β L < 1 / resources²: the constraint binds exactly where resources are small enough, and resources = income + (1+r)·assets rises with BOTH the income draw and the asset position.