The Bellman operator of a deterministic dynamic program

The operator

T v s = sup { r (s, a) + β * v (g (s, a)) | a ∈ Γ s }

is shown to map bounded continuous functions to bounded continuous functions, and to satisfy Blackwell's sufficient conditions. Combined with LeanEconomics.Blackwell this gives the value function of the program, its uniqueness, and convergence of value function iteration.

The formulation

A program is given by a feasible correspondence Γ : S → Set A with nonempty compact values that is continuous -- upper and lower hemicontinuous -- together with a bounded continuous reward r : (S × A) →ᵇ ℝ, a continuous law of motion g : C(S × A, S), and a discount factor β < 1.

The feasible set moves with the state, which is what a budget constraint does. The price of that generality is the continuity of T v, and it is paid by Berge's maximum theorem in LeanEconomics.Topology.Berge: continuous_maxValue is exactly the statement that the value of a parametrised maximisation problem is continuous in the parameter.

Verifying that a particular Γ is hemicontinuous is real work, done per model. The two programs in LeanEconomics.DynamicProgramming.Examples discharge it in the two cheapest ways: a constraint set that does not move, and one pinned to a single continuously varying point.

Main definitions

• LeanEconomics.DynamicProgram : the data of a deterministic dynamic program.
• LeanEconomics.DynamicProgram.bellman : its Bellman operator on S →ᵇ ℝ.
• LeanEconomics.DynamicProgram.valueFunction : the value function.

Main results

• LeanEconomics.DynamicProgram.blackwell : the Bellman operator satisfies Blackwell's conditions, hence is a contraction.
• LeanEconomics.DynamicProgram.bellman_valueFunction, LeanEconomics.DynamicProgram.eq_valueFunction : the value function is the unique solution of the Bellman equation.
• LeanEconomics.DynamicProgram.exists_optimal_action : the supremum is attained, so a greedy policy exists.

References

• Stokey, Lucas and Prescott, Recursive Methods in Economic Dynamics, chapter 4.

structure LeanEconomics.DynamicProgram (S : Type u_3) (A : Type u_4) [TopologicalSpace S] [TopologicalSpace A] : Type (max u_3 u_4)

A deterministic dynamic program: the agent observes a state, picks an action from the feasible set at that state, collects a reward, and moves to the state the law of motion dictates.

• feasible : S → Set A

  The actions available to the agent, as a function of the state.

• isCompact_feasible (s : S) : IsCompact (self.feasible s)

  Each feasible set is compact, so that the supremum over it is attained.

• feasible_nonempty (s : S) : (self.feasible s).Nonempty

  The agent always has something to do.

• upperHemicontinuous_feasible : UpperHemicontinuous self.feasible

  The feasible set does not explode as the state moves.

• lowerHemicontinuous_feasible : LowerHemicontinuous self.feasible

  The feasible set does not collapse as the state moves.

• reward : BoundedContinuousFunction (S × A) ℝ

  The one-period reward, bounded and continuous in state and action jointly.

• transition : C(S × A, S)

  The law of motion.

• discount : NNReal

  The discount factor.

• discount_lt_one : self.discount < 1

  Future rewards are discounted strictly, which is what makes the operator a contraction.

noncomputable def LeanEconomics.DynamicProgram.objective {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) (a : A) : ℝ

What the agent gets from action a in state s: this period's reward plus the discounted continuation value at the state the action leads to.

Equations

• D.objective v s a = D.reward (s, a) + ↑D.discount * v (D.transition (s, a))

theorem LeanEconomics.DynamicProgram.continuous_uncurry_objective {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) : Continuous ↿(D.objective v)

theorem LeanEconomics.DynamicProgram.abs_objective_le {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) (a : A) : |D.objective v s a| ≤ ‖D.reward‖ + ↑D.discount * ‖v‖

The objective is bounded uniformly in the state and the action, by the size of the reward plus the discounted size of the continuation value.

noncomputable def LeanEconomics.DynamicProgram.bellmanFn {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) : ℝ

The Bellman operator as a bare function: the value of the one-period problem, in the sense of LeanEconomics.maxValue.

Equations

• D.bellmanFn v s = LeanEconomics.maxValue (D.objective v) D.feasible s

theorem LeanEconomics.DynamicProgram.le_bellmanFn {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) {s : S} {a : A} (ha : a ∈ D.feasible s) : D.objective v s a ≤ D.bellmanFn v s

theorem LeanEconomics.DynamicProgram.bellmanFn_le {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) {s : S} {c : ℝ} (h : ∀ a ∈ D.feasible s, D.objective v s a ≤ c) : D.bellmanFn v s ≤ c

theorem LeanEconomics.DynamicProgram.abs_bellmanFn_le {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) : |D.bellmanFn v s| ≤ ‖D.reward‖ + ↑D.discount * ‖v‖

noncomputable def LeanEconomics.DynamicProgram.bellman {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) : BoundedContinuousFunction S ℝ

The Bellman operator on bounded continuous functions. Continuity of the image is Berge's maximum theorem; boundedness is abs_bellmanFn_le.

Equations

• D.bellman v = BoundedContinuousFunction.ofNormedAddCommGroup (D.bellmanFn v) ⋯ (‖D.reward‖ + ↑D.discount * ‖v‖) ⋯

@[simp]

theorem LeanEconomics.DynamicProgram.bellman_apply {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) : (D.bellman v) s = maxValue (D.objective v) D.feasible s

theorem LeanEconomics.DynamicProgram.blackwell {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) : Blackwell D.discount D.bellman

The Bellman operator satisfies Blackwell's sufficient conditions. Monotonicity holds because a larger continuation value raises the objective at every action; discounting holds because the continuation value enters multiplied by β.

theorem LeanEconomics.DynamicProgram.exists_optimal_action {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) : ∃ a ∈ D.feasible s, (D.bellman v) s = D.objective v s a ∧ ∀ b ∈ D.feasible s, D.objective v s b ≤ D.objective v s a

The supremum defining the Bellman operator is attained: in every state there is an optimal action. This is what makes a greedy policy well defined.

theorem LeanEconomics.DynamicProgram.upperHemicontinuous_argmax {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) : UpperHemicontinuous (argmax (D.objective v) D.feasible)

The maximiser correspondence of the one-period problem is upper hemicontinuous, by the second half of Berge's theorem.

theorem LeanEconomics.DynamicProgram.monotone_bellman {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) [Preorder S] (hfeas : ∀ (s s' : S), s ≤ s' → D.feasible s ⊆ D.feasible s') (hreward : ∀ (a : A), Monotone fun (s : S) => D.reward (s, a)) (htrans : ∀ (a : A), Monotone fun (s : S) => D.transition (s, a)) (v : BoundedContinuousFunction S ℝ) (hv : Monotone ⇑v) : Monotone ⇑(D.bellman v)

The Bellman operator preserves monotonicity when the feasible set grows with the state, the reward rises with it, and the law of motion is monotone in it.

theorem LeanEconomics.DynamicProgram.concaveOn_bellman {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) [AddCommMonoid S] [Module ℝ S] [AddCommMonoid A] [Module ℝ A] {s : Set S} (hs : Convex ℝ s) (hgraph : ∀ x ∈ s, ∀ y ∈ s, ∀ ax ∈ D.feasible x, ∀ ay ∈ D.feasible y, ∀ (θ φ : ℝ), 0 ≤ θ → 0 ≤ φ → θ + φ = 1 → θ • ax + φ • ay ∈ D.feasible (θ • x + φ • y)) (hreward : ∀ x ∈ s, ∀ y ∈ s, ∀ ax ∈ D.feasible x, ∀ ay ∈ D.feasible y, ∀ (θ φ : ℝ), 0 ≤ θ → 0 ≤ φ → θ + φ = 1 → θ • D.reward (x, ax) + φ • D.reward (y, ay) ≤ D.reward (θ • x + φ • y, θ • ax + φ • ay)) (htrans : ∀ (x y : S) (ax ay : A) (θ φ : ℝ), D.transition (θ • x + φ • y, θ • ax + φ • ay) = θ • D.transition (x, ax) + φ • D.transition (y, ay)) (hinv : ∀ x ∈ s, ∀ a ∈ D.feasible x, D.transition (x, a) ∈ s) (v : BoundedContinuousFunction S ℝ) (hv : ConcaveOn ℝ s ⇑v) : ConcaveOn ℝ s ⇑(D.bellman v)

The Bellman operator preserves concavity on a convex set s, given that the feasible graph is convex over s, the reward is concave along it, the law of motion is affine, and s is forward invariant.

The mixed action is feasible at the mixed state, so it is available; the value at the mixed state is at least what it delivers, which by concavity of the reward and of the continuation value is at least the mixture of the two optimal values.

noncomputable def LeanEconomics.DynamicProgram.valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) : BoundedContinuousFunction S ℝ

The value function of the program: the unique fixed point of its Bellman operator.

Equations

• D.valueFunction = ⋯.valueFunction ⋯

theorem LeanEconomics.DynamicProgram.bellman_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) : D.bellman D.valueFunction = D.valueFunction

The value function satisfies the Bellman equation.

theorem LeanEconomics.DynamicProgram.eq_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) {v : BoundedContinuousFunction S ℝ} (hv : D.bellman v = v) : v = D.valueFunction

The Bellman equation has no other bounded continuous solution.

theorem LeanEconomics.DynamicProgram.tendsto_iterate_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) : Filter.Tendsto (fun (n : ℕ) => D.bellman^[n] v) Filter.atTop (nhds D.valueFunction)

Value function iteration converges to the value function from any starting guess.

theorem LeanEconomics.DynamicProgram.norm_iterate_sub_valueFunction_le {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (v : BoundedContinuousFunction S ℝ) (n : ℕ) : ‖D.bellman^[n] v - D.valueFunction‖ ≤ ↑D.discount ^ n / (1 - ↑D.discount) * ‖D.bellman v - v‖

The geometric error bound for value function iteration on a dynamic program.

theorem LeanEconomics.DynamicProgram.exists_optimal_policy {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) (s : S) : ∃ a ∈ D.feasible s, D.valueFunction s = D.reward (s, a) + ↑D.discount * D.valueFunction (D.transition (s, a))

In every state, the value function is attained by some feasible action: the optimal policy exists, and the value function is the reward it collects plus the discounted value of the state it leads to.

theorem LeanEconomics.DynamicProgram.monotone_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) [Preorder S] (hfeas : ∀ (s s' : S), s ≤ s' → D.feasible s ⊆ D.feasible s') (hreward : ∀ (a : A), Monotone fun (s : S) => D.reward (s, a)) (htrans : ∀ (a : A), Monotone fun (s : S) => D.transition (s, a)) : Monotone ⇑D.valueFunction

The value function is increasing in the state when the feasible set grows with the state, the reward rises with it, and the law of motion is monotone in it.

theorem LeanEconomics.DynamicProgram.concaveOn_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : DynamicProgram S A) [AddCommMonoid S] [Module ℝ S] [AddCommMonoid A] [Module ℝ A] {s : Set S} (hs : Convex ℝ s) (hgraph : ∀ x ∈ s, ∀ y ∈ s, ∀ ax ∈ D.feasible x, ∀ ay ∈ D.feasible y, ∀ (θ φ : ℝ), 0 ≤ θ → 0 ≤ φ → θ + φ = 1 → θ • ax + φ • ay ∈ D.feasible (θ • x + φ • y)) (hreward : ∀ x ∈ s, ∀ y ∈ s, ∀ ax ∈ D.feasible x, ∀ ay ∈ D.feasible y, ∀ (θ φ : ℝ), 0 ≤ θ → 0 ≤ φ → θ + φ = 1 → θ • D.reward (x, ax) + φ • D.reward (y, ay) ≤ D.reward (θ • x + φ • y, θ • ax + φ • ay)) (htrans : ∀ (x y : S) (ax ay : A) (θ φ : ℝ), D.transition (θ • x + φ • y, θ • ax + φ • ay) = θ • D.transition (x, ax) + φ • D.transition (y, ay)) (hinv : ∀ x ∈ s, ∀ a ∈ D.feasible x, D.transition (x, a) ∈ s) : ConcaveOn ℝ s ⇑D.valueFunction

The value function is concave on s under those conditions.