Dynamic programs with extended-real rewards

The reward may take the value -∞, as log c does at zero consumption. The value function stays real-valued and bounded, so the contraction theory applies unchanged.

What this is for

Every model in this library that handles utility unbounded below does it with a floor: replace u by max floor u, which is bounded, and then prove separately that the floor never binds at an optimum. That argument has to be redone per model, and it fails outright once the state space is unbounded, because the bound on the value function that it needs is itself inflated by the floor. Admitting -∞ removes the device rather than working around it.

Why the value function is still bounded

Two hypotheses do it, and both are economically ordinary:

• reward_le bounds the reward above on the feasible graph. Only there: off it the reward may do anything, which matters because an action outside the budget set typically has no sensible reward at all.
• select is a continuous feasible policy whose reward is bounded below by rewardMin. This says the agent always has some decent option -- it never faces a situation where every available action is catastrophic. Without it the value would be -∞ and there would be nothing to compute.

Between them the supremum sits in [rewardMin - β‖v‖, rewardMax + β‖v‖], so it is finite, and EReal.toReal turns it back into a bounded continuous real function.

Main results

• LeanEconomics.ExtendedProgram.blackwell : the operator is a contraction.
• LeanEconomics.ExtendedProgram.exists_optimal_policy : the value function satisfies the Bellman equation, with the reward appearing as an EReal and no floor anywhere.

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

A 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, continuous into the extended reals and 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.

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

  Its reward is bounded below: the agent always has a decent option.

• le_reward_select (s : S) : ↑self.rewardMin ≤ self.reward (s, self.select s)
• transition : C(S × A, S)

  The law of motion.

• discount : NNReal

  The factor applied to next-period value.

• discount_lt_one : self.discount < 1

Extending a utility by -∞

Retrofitting a model that uses a floor means turning its real-valued u, which is only sensible on positive consumption, into a continuous EReal-valued reward. That is this lemma, and it is the only shared cost of the retrofit: supply u falling to -∞ at zero and the extension is continuous.

noncomputable def LeanEconomics.extendBot (u : ℝ → ℝ) : ℝ → EReal

A function on the positives, extended by -∞ to the whole line.

Equations

• LeanEconomics.extendBot u c = if 0 < c then ↑(u c) else ⊥

@[simp]

theorem LeanEconomics.extendBot_of_pos {u : ℝ → ℝ} {c : ℝ} (hc : 0 < c) : extendBot u c = ↑(u c)

@[simp]

theorem LeanEconomics.extendBot_of_nonpos {u : ℝ → ℝ} {c : ℝ} (hc : c ≤ 0) : extendBot u c = ⊥

theorem LeanEconomics.extendBot_mono {u : ℝ → ℝ} (hu : MonotoneOn u (Set.Ioi 0)) : Monotone (extendBot u)

The extension is monotone when u is monotone on the positives.

theorem LeanEconomics.continuous_extendBot {u : ℝ → ℝ} (hcont : ContinuousOn u (Set.Ioi 0)) (hbot : Filter.Tendsto u (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot) : Continuous (extendBot u)

The extension is continuous exactly when u falls to -∞ at zero consumption -- which is what makes a floor necessary in the first place, so nothing extra is being assumed.

noncomputable def LeanEconomics.ExtendedProgram.objectiveE {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (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 * v (D.transition (s, a)))

noncomputable def LeanEconomics.ExtendedProgram.maxE {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (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.ExtendedProgram.hiBound {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (v : BoundedContinuousFunction S ℝ) : ℝ

The upper bound on the one-period value.

Equations

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

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

The lower bound on the one-period value, coming from the feasible selection.

Equations

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

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

theorem LeanEconomics.ExtendedProgram.abs_discount_smul_le {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (v : BoundedContinuousFunction S ℝ) (t : S) : |↑D.discount * v t| ≤ ↑D.discount * ‖v‖

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

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

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

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

noncomputable def LeanEconomics.ExtendedProgram.bellmanFn {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (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.ExtendedProgram.coe_bellmanFn {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (v : BoundedContinuousFunction S ℝ) (s : S) : ↑(D.bellmanFn v s) = D.maxE v s

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

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

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

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

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

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

The Bellman operator on bounded continuous functions, with an extended-real reward.

Equations

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

@[simp]

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

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

Blackwell's conditions hold. The extended-real reward is a common summand on both sides of each inequality, so it plays no part: monotonicity and discounting are facts about the continuation term alone.

theorem LeanEconomics.ExtendedProgram.exists_optimal_action {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (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.ExtendedProgram.upperHemicontinuous_argmax {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram S A) (v : BoundedContinuousFunction S ℝ) : UpperHemicontinuous (argmax (D.objectiveE v) D.feasible)

The maximiser correspondence is upper hemicontinuous, by the argmax half of Berge for extended-real objectives.

theorem LeanEconomics.ExtendedProgram.monotone_bellman {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram 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 operator preserves monotonicity under the same conditions as in the real case.

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

The value function of the program.

Equations

• D.valueFunction = ⋯.valueFunction ⋯

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

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

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

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

The Bellman equation, with the reward an extended real and no floor anywhere.

theorem LeanEconomics.ExtendedProgram.monotone_valueFunction {S : Type u_1} {A : Type u_2} [TopologicalSpace S] [TopologicalSpace A] (D : ExtendedProgram 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 monotone under the same conditions as in the real case.