Stochastic dynamic programs with extended-real rewards

LeanEconomics.DynamicProgramming.Extended allows a reward of -∞ but has a deterministic law of motion; LeanEconomics.DynamicProgramming.Stochastic has finitely many shocks but a real-valued reward. This file is the combination, and it is what a stochastic model with log or CRRA utility needs if it is not to carry a floor.

Why the combination is routine

The expectation ∑ z, p z * v (g z) is a sum of real numbers, since value functions stay real-valued. So the objective is again reward + ↑(real): an extended real plus a finite coercion, exactly the shape Extended already handles. Neither half has to be redone -- the reward's -∞ never meets the expectation's arithmetic, and ⊥ + ⊤ never arises.

Accordingly the two facts about the expectation are the same two as in the real stochastic file: prob_nonneg gives monotonicity, prob_sum gives discounting.

Main results

• LeanEconomics.ExtendedStochasticProgram.blackwell : the operator is a contraction.
• LeanEconomics.ExtendedStochasticProgram.exists_optimal_policy : the stochastic Bellman equation, with the reward an extended real and no floor.

structure LeanEconomics.ExtendedStochasticProgram (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 whose reward may be -∞.

• 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 : C(S × A, EReal)

  The reward, possibly -∞.

• rewardMax : ℝ

  An upper bound on the reward, needed only on the feasible graph.

• reward_le (s : S) (a : A) : a ∈ self.feasible s → self.reward (s, a) ≤ ↑self.rewardMax
• select : C(S, A)

  A continuous feasible policy whose reward is bounded below.

• select_mem (s : S) : self.select s ∈ self.feasible s
• rewardMin : ℝ

  A uniform one-period payoff available through the feasible policy select.

• le_reward_select (s : S) : ↑self.rewardMin ≤ self.reward (s, self.select s)
• 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.ExtendedStochasticProgram.expect {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (p : S × A) : ℝ

The expected continuation value: a sum of reals, so it never meets the reward's -∞.

Equations

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

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

The objective, in the extended reals.

Equations

• D.objectiveE v s a = D.reward (s, a) + ↑(↑D.discount * D.expect v (s, a))

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

The value of the one-period problem, in the extended reals.

Equations

• D.maxE v s = LeanEconomics.maxValueE (D.objectiveE v) D.feasible s

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

The upper bound on the one-period value.

Equations

• D.hiBound v = D.rewardMax + ↑D.discount * ‖v‖

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

The lower bound on the one-period value.

Equations

• D.loBound v = D.rewardMin - ↑D.discount * ‖v‖

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

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

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

An average of values of v is no larger than the size of v.

theorem LeanEconomics.ExtendedStochasticProgram.maxE_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : D.maxE v s ≤ ↑(D.hiBound v)

theorem LeanEconomics.ExtendedStochasticProgram.le_maxE {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : ↑(D.loBound v) ≤ D.maxE v s

theorem LeanEconomics.ExtendedStochasticProgram.maxE_ne_top {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : D.maxE v s ≠ ⊤

theorem LeanEconomics.ExtendedStochasticProgram.maxE_ne_bot {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : D.maxE v s ≠ ⊥

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

The Bellman operator as a bare real-valued function.

Equations

• D.bellmanFn v s = (D.maxE v s).toReal

@[simp]

theorem LeanEconomics.ExtendedStochasticProgram.coe_bellmanFn {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : ↑(D.bellmanFn v s) = D.maxE v s

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

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

theorem LeanEconomics.ExtendedStochasticProgram.bellmanFn_bounds {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : D.loBound v ≤ D.bellmanFn v s ∧ D.bellmanFn v s ≤ D.hiBound v

theorem LeanEconomics.ExtendedStochasticProgram.abs_bellmanFn_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : |D.bellmanFn v s| ≤ max |D.loBound v| |D.hiBound v|

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

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

The stochastic Bellman operator with an extended-real reward.

Equations

• D.bellman v = BoundedContinuousFunction.ofNormedAddCommGroup (D.bellmanFn v) ⋯ (max |D.loBound v| |D.hiBound v|) ⋯

@[simp]

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

theorem LeanEconomics.ExtendedStochasticProgram.expect_add_const {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (c : ℝ) (p : S × A) : D.expect (v + BoundedContinuousFunction.const S c) p = D.expect v p + c

Adding a constant to the continuation value adds exactly that constant to the expectation: this is prob_sum.

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

Blackwell's conditions hold.

theorem LeanEconomics.ExtendedStochasticProgram.exists_optimal_action {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) (s : S) : ∃ a ∈ D.feasible s, D.objectiveE v s a = ↑(D.bellmanFn v s)

The supremum is attained: an optimal action exists at every state.

theorem LeanEconomics.ExtendedStochasticProgram.upperHemicontinuous_argmax {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (v : BoundedContinuousFunction S ℝ) : UpperHemicontinuous (argmax (D.objectiveE v) D.feasible)

The maximiser correspondence is upper hemicontinuous.

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

The value function of the program.

Equations

• D.valueFunction = ⋯.valueFunction ⋯

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

theorem LeanEconomics.ExtendedStochasticProgram.norm_valueFunction_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) : ‖D.valueFunction‖ ≤ max |D.rewardMin| |D.rewardMax| / (1 - ↑D.discount)

An explicit bound on the value function, in terms of the reward bounds alone.

The right-hand side mentions no state and no fixed point, which is exactly what is needed to make bounds derived from ‖valueFunction‖ uniform across a FAMILY of programs: the reward bounds of a family are typically easy to control, whereas its value functions are not.

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

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

theorem LeanEconomics.ExtendedStochasticProgram.bellman_const_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) {c : ℝ} (hc : D.rewardMax + ↑D.discount * c ≤ c) : D.bellman (BoundedContinuousFunction.const S c) ≤ BoundedContinuousFunction.const S c

The constant plan is not improved on by the operator, so value function iteration started there stays below it.

theorem LeanEconomics.ExtendedStochasticProgram.le_bellman_const {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) {c : ℝ} (hc : c ≤ D.rewardMin + ↑D.discount * c) : BoundedContinuousFunction.const S c ≤ D.bellman (BoundedContinuousFunction.const S c)

theorem LeanEconomics.ExtendedStochasticProgram.valueFunction_le_const {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) {c : ℝ} (hc : D.rewardMax + ↑D.discount * c ≤ c) (s : S) : D.valueFunction s ≤ c

The value function never exceeds the best constant plan. Unlike norm_valueFunction_le this is one-sided, and the pair of bounds caps the OSCILLATION of the value function by (rewardMax - rewardMin) / (1 - β) -- a quantity that does not move when a constant is added to the reward, which the sup norm does. That matters for CES: c ^ (1-γ) / (1-γ) differs from log by the constant 1 / (1-γ), so any bound built from ‖V‖ blows up as γ → 1 while the model it describes does not.

theorem LeanEconomics.ExtendedStochasticProgram.const_le_valueFunction {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) {c : ℝ} (hc : c ≤ D.rewardMin + ↑D.discount * c) (s : S) : c ≤ D.valueFunction s

theorem LeanEconomics.ExtendedStochasticProgram.valueFunction_le_of_bellman_le_on {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D₁ D₂ : ExtendedStochasticProgram S A Z) (C : BoundedContinuousFunction S ℝ → Prop) (hC0 : C 0) (hC : ∀ (v : BoundedContinuousFunction S ℝ), C v → C (D₁.bellman v)) (hle : ∀ (v : BoundedContinuousFunction S ℝ), C v → ⇑(D₁.bellman v) ≤ ⇑(D₂.bellman v)) (s : S) : D₁.valueFunction s ≤ D₂.valueFunction s

A dominated operator has a dominated value function, on an invariant class. The domination need only hold on a class of continuation values that contains 0 and that the dominated operator preserves, since value function iteration from 0 never leaves it. That is what lets the discount factor be compared: a more patient agent's operator dominates only on NONNEGATIVE continuation values, which is exactly the class the iteration stays in when the reward is nonnegative.

theorem LeanEconomics.ExtendedStochasticProgram.zero_le_bellman {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram S A Z) (hmin : 0 ≤ D.rewardMin) {v : BoundedContinuousFunction S ℝ} (hv : 0 ≤ ⇑v) : 0 ≤ ⇑(D.bellman v)

Nonnegative rewards give a nonnegative value.

theorem LeanEconomics.ExtendedStochasticProgram.valueFunction_le_of_bellman_le {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D₁ D₂ : ExtendedStochasticProgram S A Z) (hle : ∀ (v : BoundedContinuousFunction S ℝ), ⇑(D₁.bellman v) ≤ ⇑(D₂.bellman v)) (s : S) : D₁.valueFunction s ≤ D₂.valueFunction s

A dominated operator has a dominated value function. The comparative-statics workhorse, at the level the models use: comparing two economies reduces to comparing their Bellman operators at a common continuation value.

theorem LeanEconomics.ExtendedStochasticProgram.exists_optimal_policy {S : Type u_1} {A : Type u_2} {Z : Type u_3} [TopologicalSpace S] [TopologicalSpace A] [Fintype Z] (D : ExtendedStochasticProgram 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, with the reward an extended real and no floor.