Corollary 9.2.4 — the two degenerate cases
ProvedMDPFinance.DividendProblems.corollary_9_2_4dynamic-programmingmarkov-decision-processrisk-theory
Two sign-definite special cases of Theorem 9.2.3 a), each with an easy economic explanation given in the book's own text: if the reserve's increments are never positive, paying out everything immediately and stopping is optimal (); if they are never negative, ruin is impossible but discounting still makes paying out as fast as possible optimal ().
Moderation note. Part b) was vacuous in the draft because the model carried ℙ(Z < 0) > 0 as a field; with that assumption moved out of the structure it is now a genuine statement. Both parts state f^*(x) = x⁺ for all x, as the book does; probabilities are compared in [0,∞] rather than through toReal.
Preamble
import Mathlib import Definitions.Def_MDPFinance_DividendProblems_MDM import Definitions.Def_MDPFinance_DividendProblems_Dividend open scoped ENNReal NNReal open MeasureTheory ProbabilityTheory
Formal statement
namespace MDPFinance.DividendProblems
/-- Corollary 9.2.4 (Bäuerle–Rieder, p. 275, PDF 285). a) If `\mathbb P(Z \le 0) = 1` then
`J_\infty(x) = x^+` and `f^*(x) = x^+`. b) If `\mathbb P(Z \ge 0) = 1` then `J_\infty(x) = x +
\beta\mathbb EZ/(1-\beta)` for `x \ge 0` and `f^*(x) = x^+`. -/
theorem corollary_9_2_4 (M : DividendModel) (fstar : ℤ → ℕ) (hfstar : M.IsLargestMaximizer fstar) :
(M.Zpmf.toMeasure {k : ℤ | k ≤ 0} = 1 →
(∀ x : ℤ, M.Jinf x = ((max x 0).toNat : ℝ≥0∞)) ∧ ∀ x : ℤ, (fstar x : ℤ) = max x 0) ∧
(M.Zpmf.toMeasure {k : ℤ | 0 ≤ k} = 1 →
(∀ x : ℤ, 0 ≤ x → M.Jinf x = ENNReal.ofReal ((x : ℝ) + M.β * M.EZ / (1 - M.β))) ∧
∀ x : ℤ, (fstar x : ℤ) = max x 0) := by sorry
end MDPFinance.DividendProblems
Source
Bäuerle and Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer 2011, DOI 10.1007/978-3-642-18324-9, p. 275, PDF 285, Corollary 9.2.4
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.