The optimal policy is increasing in assets

A household that starts richer saves at least as much, holding the income state fixed.

The argument is the classical monotone-comparative-statics one, but it needs neither Topkis nor any derivative. Two observations do all the work.

First, the continuation value β E[V(a', z')] depends on the chosen saving a' and on the current income state, but not on current assets. So when comparing two asset levels with the same income state, the continuation terms cancel, and increasing differences of the objective reduces to increasing differences of u composed with the budget — which is exactly ConcaveOn.sub_le_sub_of_shift, concavity of u.

Second, the usual Topkis conclusion (the argmax is an increasing correspondence) is not needed, because uniqueness of the optimal action is already proved. If the richer household saved strictly less, the exchange argument shows the poorer household's choice is also optimal for the richer one, and uniqueness collapses the two.

The feasible set grows with assets, which is what makes both exchanges legal.

The budget grows with assets

theorem LeanEconomics.IncomeFluctuation.resources_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {a a' : ℝ} {z : Z} (h : a ≤ a') : P.resources (a, z) ≤ P.resources (a', z)

theorem LeanEconomics.IncomeFluctuation.maxSaving_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {a a' : ℝ} {z : Z} (h : a ≤ a') : P.maxSaving (a, z) ≤ P.maxSaving (a', z)

theorem LeanEconomics.IncomeFluctuation.feasible_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {a a' : ℝ} {z : Z} (h : a ≤ a') : P.toExtended.feasible (a, z) ⊆ P.toExtended.feasible (a', z)

The objective in the reals

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

The continuation value of saving x when the current income state is z. It does not depend on current assets, which is what makes the comparison below work.

Equations

• P.cont z x = ∑ z' : Z, P.transitionMatrix z z' * P.toExtended.valueFunction (x, z')

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

The objective, as a real number. Valid wherever consumption is positive.

Equations

• P.objR s x = P.u (P.consumption s x) + ↑P.discount * P.cont s.2 x

theorem LeanEconomics.IncomeFluctuation.objectiveE_eq_coe {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {x : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (hx : x ∈ P.toExtended.feasible s) (hc : P.consumption s x ∈ P.dom) : P.toExtended.objectiveE P.toExtended.valueFunction s x = ↑(P.objR s x)

theorem LeanEconomics.IncomeFluctuation.objR_le_of_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {x : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (hx : x ∈ P.toExtended.feasible s) (hc : P.consumption s x ∈ P.dom) : P.objR s x ≤ P.objR s (P.policy s)

Any feasible action with positive consumption is worth at most the optimum.

Monotonicity

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

The continuation value of saving x, read against v.

Equations

• P.contOf v z x = ∑ z' : Z, P.transitionMatrix z z' * v (x, z')

noncomputable def LeanEconomics.IncomeFluctuation.objROf {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (s : ℝ × Z) (x : ℝ) : ℝ

The objective, as a real number, read against v.

Equations

• P.objROf v s x = P.u (P.consumption s x) + ↑P.discount * P.contOf v s.2 x

theorem LeanEconomics.IncomeFluctuation.concaveOn_contOf {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) (z : Z) : ConcaveOn ℝ (Set.Icc assetFloor assetCap) (P.contOf v z)

theorem LeanEconomics.IncomeFluctuation.abs_contOf_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) (x : ℝ) : |P.contOf v z x| ≤ ‖v‖

theorem LeanEconomics.IncomeFluctuation.objectiveE_eq_coe_of {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) {a : ℝ} {z : Z} {x : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hx : x ∈ P.toExtended.feasible (a, z)) (hcx : P.consumption (a, z) x ∈ P.dom) : P.toExtended.objectiveE v (a, z) x = ↑(P.objROf v (a, z) x)

The objective in the reals agrees with the extended objective where consumption is positive.

theorem LeanEconomics.IncomeFluctuation.objROf_le_of_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) {a : ℝ} {z : Z} {x : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (hx : x ∈ P.toExtended.feasible (a, z)) (hcx : P.consumption (a, z) x ∈ P.dom) : P.objROf v (a, z) x ≤ P.objROf v (a, z) (P.policyOf v (a, z))

Any feasible action with positive consumption is worth at most the optimum, whatever the continuation.

Monotonicity of the saving policy

theorem LeanEconomics.IncomeFluctuation.policyOf_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) {a a' : ℝ} {z : Z} (ha : a ∈ Set.Icc assetFloor assetCap) (ha' : a' ∈ Set.Icc assetFloor assetCap) (hle : a ≤ a') : P.policyOf v (a, z) ≤ P.policyOf v (a', z)

The optimal policy is increasing in assets, whatever the continuation. The exchange argument uses concavity and uniqueness against v.

theorem LeanEconomics.IncomeFluctuation.policy_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {a a' : ℝ} {z : Z} (ha : a ∈ Set.Icc assetFloor assetCap) (ha' : a' ∈ Set.Icc assetFloor assetCap) (hle : a ≤ a') : P.policy (a, z) ≤ P.policy (a', z)

The optimal policy is increasing in assets. Holding the income state fixed, a household with more assets saves at least as much.

def LeanEconomics.IncomeFluctuation.OscOn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (_P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (G : ℝ) : Prop

v varies by at most G over the asset region.

Equations

• _P.OscOn v G = ∀ x ∈ Set.Icc assetFloor assetCap, ∀ y ∈ Set.Icc assetFloor assetCap, ∀ (z z' : Z), v (x, z) - v (y, z') ≤ G

theorem LeanEconomics.IncomeFluctuation.OscOn.mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {G G' : ℝ} (h : P.OscOn v G) (hG : G ≤ G') : P.OscOn v G'

theorem LeanEconomics.IncomeFluctuation.contOf_sub_le_osc {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {G : ℝ} (h : P.OscOn v G) {x y : ℝ} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) (z z' : Z) : P.contOf v z x - P.contOf v z' y ≤ G

The continuation inherits the bound, even across different income states.

theorem LeanEconomics.IncomeFluctuation.oscOn_two_norm {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : P.OscOn v (2 * ‖v‖)

A bounded continuation oscillates by at most twice its norm.

theorem LeanEconomics.IncomeFluctuation.valueFunction_le_oscBound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.toExtended.valueFunction s ≤ P.u P.maxConsumption / (1 - ↑P.discount)

theorem LeanEconomics.IncomeFluctuation.oscBound_le_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.u P.minConsumption / (1 - ↑P.discount) ≤ P.toExtended.valueFunction s

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

The spread the iteration can produce: the reward's spread, amplified by (1 - β)⁻¹. At a zero borrowing limit this is definitionally CRRAConstants.oscGap, so the witnesses' bounds on that transfer unchanged.

Equations

• P.oscSpread = (P.u P.maxConsumption - P.u P.minConsumption) / (1 - ↑P.discount)

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

theorem LeanEconomics.IncomeFluctuation.oscOn_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.OscOn P.toExtended.valueFunction P.oscSpread

The fixed-point value function satisfies the oscillation premise used by saving bounds.