Stochastic dynamic programming with finitely many shocks

The Bellman operator

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

where a shock z is drawn from a finite set with probabilities p z (s, a) and leads to the state g z (s, a). This is the deterministic operator of LeanEconomics.DynamicProgramming.Bellman with the successor state replaced by an expectation over successors.

Why this is a new structure rather than a reuse

The deterministic program's continuation is v evaluated at one point. Here it is a convex combination of v at several points, which is not of that form, so the operator has to be rebuilt. Everything above the operator is reused unchanged: the same Blackwell conditions give the contraction, and the same Berge theorem gives continuity. Only the two facts about the expectation are new, and they are exactly the two properties of a probability distribution:

• p ≥ 0 gives monotonicity -- a larger continuation value cannot lower the average;
• ∑ p = 1 gives discounting -- adding a constant to the continuation value adds exactly that constant to the average, not more.

Shock probabilities may depend on the state and the action, which covers a Markov chain on a component of the state as the special case where they depend on that component alone.

Main results

• LeanEconomics.StochasticDynamicProgram.blackwell : the operator is a contraction.
• LeanEconomics.StochasticDynamicProgram.exists_optimal_policy : the value function satisfies the stochastic Bellman equation, and the maximum is attained.

structure LeanEconomics.StochasticDynamicProgram (S : Type u_4) (A : Type u_5) (Z : Type u_6) [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] : Type (max (max u_4 u_5) u_6)

A stochastic dynamic program with finitely many shocks.

• feasible : S → Set A

  The actions available at each state.

• isCompact_feasible (s : S) : IsCompact (self.feasible s)
• feasible_nonempty (s : S) : (self.feasible s).Nonempty
• upperHemicontinuous_feasible : UpperHemicontinuous self.feasible
• lowerHemicontinuous_feasible : LowerHemicontinuous self.feasible
• reward : BoundedContinuousFunction (S × A) ℝ

  The one-period reward.

• transition : Z → C(S × A, S)

  The state reached when shock z occurs.

• prob : Z → C(S × A, ℝ)

  The probability that shock z occurs.

• prob_nonneg (z : Z) (p : S × A) : 0 ≤ (self.prob z) p
• prob_sum (p : S × A) : ∑ z : Z, (self.prob z) p = 1
• discount : NNReal

  The factor applied to next-period value.

• discount_lt_one : self.discount < 1

noncomputable def LeanEconomics.StochasticDynamicProgram.expectation {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : StochasticDynamicProgram S A Z) (v : BoundedContinuousFunction S ℝ) (p : S × A) : ℝ

The expected continuation value of v after choosing a at s.

Equations

• D.expectation v p = ∑ z : Z, (D.prob z) p * v ((D.transition z) p)

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

Current reward plus the discounted expected continuation value.

Equations

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

theorem LeanEconomics.StochasticDynamicProgram.continuous_expectation {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : StochasticDynamicProgram S A Z) (v : BoundedContinuousFunction S ℝ) : Continuous (D.expectation v)

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

theorem LeanEconomics.StochasticDynamicProgram.abs_expectation_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : StochasticDynamicProgram S A Z) (v : BoundedContinuousFunction S ℝ) (p : S × A) : |D.expectation v p| ≤ ‖v‖

An average of values of v is no larger than the size of v. This is where p ≥ 0 and ∑ p = 1 first do their work.

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

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

The Bellman operator as a bare function.

Equations

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

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

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

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

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

The stochastic Bellman operator on bounded continuous functions.

Equations

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

@[simp]

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

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

Blackwell's conditions hold. Monotonicity is prob_nonneg: averaging with nonnegative weights preserves order. Discounting is prob_sum: the weights sum to one, so raising the continuation value by c raises the average by exactly c, and the objective by β * c.

theorem LeanEconomics.StochasticDynamicProgram.exists_optimal_action {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : StochasticDynamicProgram S A Z) (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 is attained: an optimal action exists at every state.

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

The value function of the stochastic program.

Equations

• D.valueFunction = ⋯.valueFunction ⋯

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

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

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

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

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

The stochastic Bellman equation. At every state there is an optimal action, and the value is the reward it earns plus the discounted expected value of the successor state.