Blackwell's sufficient conditions

An operator on bounded continuous functions that is monotone and discounts is a contraction. This is the standard route to showing that a Bellman operator has a unique fixed point: verifying monotonicity and discounting is elementary, whereas verifying the contraction property directly is not.

The setting is the space S →ᵇ ℝ of bounded continuous real-valued functions on a state space S, with the supremum norm. It is already a complete metric space, which is what the Banach fixed point theorem needs.

Main definitions

• LeanEconomics.Blackwell β T : T is monotone and discounts at rate β.
• LeanEconomics.Blackwell.valueFunction : the unique fixed point of T.

Main results

• LeanEconomics.Blackwell.contractingWith : Blackwell's conditions imply T is a β-contraction.
• LeanEconomics.Blackwell.isFixedPt_valueFunction, LeanEconomics.Blackwell.eq_valueFunction : the value function is the unique solution of the fixed point equation T v = v.
• LeanEconomics.Blackwell.tendsto_iterate_valueFunction : value function iteration converges to it, from any starting guess.
• LeanEconomics.Blackwell.norm_iterate_sub_valueFunction_le : the geometric error bound ‖Tⁿ v - v*‖ ≤ βⁿ / (1 - β) * ‖T v - v‖, which is the stopping rule used in practice.

Examples

• LeanEconomics.Blackwell.affine : the affine operator v ↦ f + β • v satisfies the conditions. This is the degenerate case of a Bellman operator in which the agent has no choice to make, and it witnesses that the hypotheses are consistent.

References

• Stokey, Lucas and Prescott, Recursive Methods in Economic Dynamics.
• Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965).

theorem BoundedContinuousFunction.le_add_const_norm_sub {S : Type u_1} [TopologicalSpace S] (v w : BoundedContinuousFunction S ℝ) : v ≤ w + const S ‖v - w‖

Any bounded continuous function is dominated by any other one shifted up by the distance between them.

structure LeanEconomics.Blackwell {S : Type u_1} [TopologicalSpace S] (β : NNReal) (T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ) : Prop

Blackwell's sufficient conditions for an operator on bounded continuous functions to be a contraction of modulus β.

monotone says a pointwise larger continuation value cannot lower the operator's value; discounting says that raising the continuation value everywhere by a constant c raises the operator's value by at most β * c. For a Bellman operator both are immediate: the first because the objective is increasing in the continuation value, the second because the continuation value enters multiplied by the discount factor.

• monotone : Monotone T

  A pointwise larger continuation value gives a pointwise larger image.

• discounting (v : BoundedContinuousFunction S ℝ) (c : ℝ) : 0 ≤ c → T (v + BoundedContinuousFunction.const S c) ≤ T v + BoundedContinuousFunction.const S (↑β * c)

  Adding a constant c ≥ 0 to the continuation value raises the image by at most β * c.

theorem LeanEconomics.Blackwell.apply_le_add_const {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (v w : BoundedContinuousFunction S ℝ) : T v ≤ T w + BoundedContinuousFunction.const S (↑β * ‖v - w‖)

The one-sided bound at the heart of Blackwell's argument: T v cannot exceed T w by more than β times the distance between v and w.

theorem LeanEconomics.Blackwell.norm_sub_le {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (v w : BoundedContinuousFunction S ℝ) : ‖T v - T w‖ ≤ ↑β * ‖v - w‖

Blackwell's conditions make T Lipschitz with constant β in the supremum norm.

theorem LeanEconomics.Blackwell.lipschitzWith {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) : LipschitzWith β T

theorem LeanEconomics.Blackwell.contractingWith {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) : ContractingWith β T

Blackwell's theorem: a monotone operator that discounts at rate β < 1 is a contraction of modulus β.

noncomputable def LeanEconomics.Blackwell.valueFunction {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) : BoundedContinuousFunction S ℝ

The value function: the unique fixed point of an operator satisfying Blackwell's conditions, obtained from the Banach fixed point theorem.

Equations

• h.valueFunction hβ = ContractingWith.fixedPoint T ⋯

theorem LeanEconomics.Blackwell.isFixedPt_valueFunction {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) : T (h.valueFunction hβ) = h.valueFunction hβ

The value function solves the fixed point equation.

theorem LeanEconomics.Blackwell.eq_valueFunction {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) {v : BoundedContinuousFunction S ℝ} (hv : T v = v) : v = h.valueFunction hβ

The value function is the only solution of the fixed point equation.

theorem LeanEconomics.Blackwell.tendsto_iterate_valueFunction {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) (v : BoundedContinuousFunction S ℝ) : Filter.Tendsto (fun (n : ℕ) => T^[n] v) Filter.atTop (nhds (h.valueFunction hβ))

Value function iteration converges, from any starting guess.

theorem LeanEconomics.Blackwell.norm_iterate_sub_valueFunction_le {S : Type u_1} [TopologicalSpace S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) (v : BoundedContinuousFunction S ℝ) (n : ℕ) : ‖T^[n] v - h.valueFunction hβ‖ ≤ ↑β ^ n / (1 - ↑β) * ‖T v - v‖

The geometric error bound for value function iteration: after n iterations from a guess v, the distance to the value function is at most βⁿ / (1 - β) times the size of the first update. This is the a priori bound behind the usual stopping rule.

theorem LeanEconomics.Blackwell.affine {S : Type u_1} [TopologicalSpace S] (f : BoundedContinuousFunction S ℝ) (β : NNReal) : Blackwell β fun (v : BoundedContinuousFunction S ℝ) => f + ↑β • v

The affine operator v ↦ f + β • v, a dynamic program with a single feasible action, satisfies Blackwell's conditions.

theorem LeanEconomics.Blackwell.valueFunction_le {S : Type u_1} [TopologicalSpace S] {β₁ β₂ : NNReal} {T₁ T₂ : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h₁ : Blackwell β₁ T₁) (h₂ : Blackwell β₂ T₂) (hβ₁ : β₁ < 1) (hβ₂ : β₂ < 1) (hle : ∀ (v : BoundedContinuousFunction S ℝ), ⇑(T₁ v) ≤ ⇑(T₂ v)) (s : S) : (h₁.valueFunction hβ₁) s ≤ (h₂.valueFunction hβ₂) s

A dominated operator has a dominated fixed point. If one Bellman operator never returns more than another, its value function never does either.

This is the workhorse of comparative statics: to compare two economies one only has to compare their operators at a COMMON continuation value, which is a one-period calculation, and the comparison of the infinite-horizon values follows. The two need not share a discount factor. No policy comparison, no differentiability, nothing about argmaxes -- the whole content is that value function iteration started from the same place stays ordered.

Monotonicity of the value function

If the operator preserves monotone functions then so does its fixed point, because the monotone functions are a closed subset of S →ᵇ ℝ and value function iteration converges in norm. Nothing about the fixed point itself is needed, only that the property is closed and preserved. This is the standard route to comparative statics.

theorem LeanEconomics.isClosed_monotone {S : Type u_1} [TopologicalSpace S] [Preorder S] : IsClosed {v : BoundedContinuousFunction S ℝ | Monotone ⇑v}

The monotone bounded continuous functions form a closed set: a supremum-norm limit of monotone functions is monotone, since evaluation at a point is continuous.

theorem LeanEconomics.Blackwell.monotone_valueFunction {S : Type u_1} [TopologicalSpace S] [Preorder S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) (hT : ∀ (v : BoundedContinuousFunction S ℝ), Monotone ⇑v → Monotone ⇑(T v)) : Monotone ⇑(h.valueFunction hβ)

The value function is monotone whenever the operator preserves monotonicity.

Concavity of the value function

The same closed-set argument as for monotonicity, and the reason it is wanted is the agent distribution. Defining a distribution over states needs the optimal policy to be a function, and exists_optimal_action only gives existence of a maximiser. Uniqueness comes from strict concavity of the objective in the action, which needs the continuation value to be concave -- that is, the value function. So this is the first link in the chain from the value function to the stationary distribution.

theorem LeanEconomics.isClosed_concaveOn {S : Type u_2} [TopologicalSpace S] [AddCommMonoid S] [Module ℝ S] {s : Set S} (hs : Convex ℝ s) : IsClosed {v : BoundedContinuousFunction S ℝ | ConcaveOn ℝ s ⇑v}

The functions concave on a fixed convex set form a closed set.

Stated on a set rather than the whole space deliberately. The household models clamp assets with max 0 a, which is convex and so breaks concavity globally -- but max 0 a = a on [0, ā], so concavity does hold on the compact convex region the economics lives in, and that is the region the agent distribution will be supported on.

theorem LeanEconomics.Blackwell.concaveOn_valueFunction {S : Type u_2} [TopologicalSpace S] [AddCommMonoid S] [Module ℝ S] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} {s : Set S} (hs : Convex ℝ s) (h : Blackwell β T) (hβ : β < 1) (hT : ∀ (v : BoundedContinuousFunction S ℝ), ConcaveOn ℝ s ⇑v → ConcaveOn ℝ s ⇑(T v)) : ConcaveOn ℝ s ⇑(h.valueFunction hβ)

The value function is concave on s whenever the operator preserves concavity on s.

Concavity along slices

A stochastic household's state is a pair (assets, income state), and that is not a module over ℝ -- there is no sensible convex combination of income states. So concavity cannot be stated on the state space itself. What is wanted, and what is true, is concavity in assets for each fixed income state, which is concavity along a family of slices. It is still a closed condition, so the same argument applies.

theorem LeanEconomics.isClosed_forall_concaveOn {S : Type u_1} [TopologicalSpace S] {ι : Type u_2} {E : Type u_3} [AddCommMonoid E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) (g : ι → E → S) : IsClosed {v : BoundedContinuousFunction S ℝ | ∀ (i : ι), ConcaveOn ℝ s fun (e : E) => v (g i e)}

Concavity along every slice is a closed condition.

theorem LeanEconomics.Blackwell.forall_concaveOn_valueFunction {S : Type u_1} [TopologicalSpace S] {ι : Type u_2} {E : Type u_3} [AddCommMonoid E] [Module ℝ E] {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} {s : Set E} (hs : Convex ℝ s) (g : ι → E → S) (h : Blackwell β T) (hβ : β < 1) (hT : ∀ (v : BoundedContinuousFunction S ℝ), (∀ (i : ι), ConcaveOn ℝ s fun (e : E) => v (g i e)) → ∀ (i : ι), ConcaveOn ℝ s fun (e : E) => (T v) (g i e)) (i : ι) : ConcaveOn ℝ s fun (e : E) => (h.valueFunction hβ) (g i e)

The value function is concave along every slice whenever the operator preserves that.

Lipschitz value functions

The third closed class, after monotone and concave. A value function that is Lipschitz in one coordinate is what lets a marginal argument run without derivatives: it bounds the marginal value of that coordinate uniformly, which is what a corner condition needs.

As with concavity, the property is stated along a family of slices g i, since the state space need not be a metric space in the coordinate of interest.

theorem LeanEconomics.isClosed_forall_lipschitzOn {S : Type u_2} [TopologicalSpace S] {ι : Type u_3} (t : Set ℝ) (L : ℝ) (g : ι → ℝ → S) : IsClosed {v : BoundedContinuousFunction S ℝ | ∀ (i : ι), ∀ x ∈ t, ∀ y ∈ t, |v (g i x) - v (g i y)| ≤ L * |x - y|}

theorem LeanEconomics.Blackwell.forall_lipschitzOn_valueFunction {S : Type u_2} [TopologicalSpace S] {ι : Type u_3} {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) {t : Set ℝ} {L : ℝ} (hL : 0 ≤ L) {g : ι → ℝ → S} (hT : ∀ (v : BoundedContinuousFunction S ℝ), (∀ (i : ι), ∀ x ∈ t, ∀ y ∈ t, |v (g i x) - v (g i y)| ≤ L * |x - y|) → ∀ (i : ι), ∀ x ∈ t, ∀ y ∈ t, |(T v) (g i x) - (T v) (g i y)| ≤ L * |x - y|) (i : ι) (x : ℝ) : x ∈ t → ∀ y ∈ t, |(h.valueFunction hβ) (g i x) - (h.valueFunction hβ) (g i y)| ≤ L * |x - y|

The value function is Lipschitz along the slices whenever the operator preserves that property. The nonnegativity of L is what makes the zero function a valid starting point for the iteration.

Increasing differences

The fourth closed class, after monotone, concave and Lipschitz.

A function of two real coordinates has increasing differences when raising the second coordinate raises the increment in the first. For a value function whose coordinates are assets and the interest rate, that says the marginal value of wealth rises with the rate -- and that is the derivative-free form of the condition driving Light (2018) Theorem 1, where it appears as f'(·, R₂) ≥ f'(·, R₁) and is obtained from the envelope theorem.

Stating it as increments rather than derivatives is what makes it expressible here at all, since nothing in this development differentiates anything. Its natural home is the augmented programme of Models/IncomeFluctuationAugmented.lean, where the rate is a state coordinate, so the property is about a single function rather than a family.

Whether the Bellman operator preserves it is a separate question and is NOT settled here; Light's argument for the derivative version compares different asset levels across rates via a rescaling, so it does not transcribe.

theorem LeanEconomics.isClosed_forall_increasingDifferences {S : Type u_2} [TopologicalSpace S] {ι : Type u_3} (s t : Set ℝ) (g : ι → ℝ → ℝ → S) : IsClosed {v : BoundedContinuousFunction S ℝ | ∀ (i : ι), ∀ a₁ ∈ s, ∀ a₂ ∈ s, ∀ r₁ ∈ t, ∀ r₂ ∈ t, a₁ ≤ a₂ → r₁ ≤ r₂ → v (g i a₂ r₁) - v (g i a₁ r₁) ≤ v (g i a₂ r₂) - v (g i a₁ r₂)}

theorem LeanEconomics.Blackwell.forall_increasingDifferences_valueFunction {S : Type u_2} [TopologicalSpace S] {ι : Type u_3} {β : NNReal} {T : BoundedContinuousFunction S ℝ → BoundedContinuousFunction S ℝ} (h : Blackwell β T) (hβ : β < 1) {s t : Set ℝ} {g : ι → ℝ → ℝ → S} (hT : ∀ (v : BoundedContinuousFunction S ℝ), (∀ (i : ι), ∀ a₁ ∈ s, ∀ a₂ ∈ s, ∀ r₁ ∈ t, ∀ r₂ ∈ t, a₁ ≤ a₂ → r₁ ≤ r₂ → v (g i a₂ r₁) - v (g i a₁ r₁) ≤ v (g i a₂ r₂) - v (g i a₁ r₂)) → ∀ (i : ι), ∀ a₁ ∈ s, ∀ a₂ ∈ s, ∀ r₁ ∈ t, ∀ r₂ ∈ t, a₁ ≤ a₂ → r₁ ≤ r₂ → (T v) (g i a₂ r₁) - (T v) (g i a₁ r₁) ≤ (T v) (g i a₂ r₂) - (T v) (g i a₁ r₂)) (i : ι) (a₁ : ℝ) : a₁ ∈ s → ∀ a₂ ∈ s, ∀ r₁ ∈ t, ∀ r₂ ∈ t, a₁ ≤ a₂ → r₁ ≤ r₂ → (h.valueFunction hβ) (g i a₂ r₁) - (h.valueFunction hβ) (g i a₁ r₁) ≤ (h.valueFunction hβ) (g i a₂ r₂) - (h.valueFunction hβ) (g i a₁ r₂)

The value function has increasing differences whenever the operator preserves the property. The zero function has it trivially, which is what lets the iteration start.