Extended Bellman Equations for Spectral Finance: Per-Mode Convergence, Shadow Prices, and Model-Free Bounds
Abstract
The Bellman equation \(V = \max_a [R + \gamma \sum P V]\) is the foundation of dynamic programming, yet its standard form obscures three structural properties critical for financial applications. We prove three extensions — spectral, constrained, and robust — and derive their finance applications, all machine-verified in Lean 4.
(1) Spectral Bellman. Decomposing the value function into eigenmodes of the transition kernel \(P\) yields \(N\) independent scalar recurrences \(v_k' = r_k + \gamma \mu_k v_k\), where \(\mu_k\) are the eigenvalues of \(P\). Each mode \(k\) contracts at rate \(\gamma |\mu_k| \leq \gamma\). Fast-decaying modes (\(|\mu_k| \ll 1\)) converge in a single iteration; truncating them has bounded error. The Fourier-cosine (COS) backward step for option pricing is this per-mode Bellman — the characteristic function values play the role of eigenvalues (Theorem 4).
(2) Constrained Bellman. Adding risk constraints \(C(s) \leq b\) to the MDP yields a Lagrangian \(L = V + \lambda(b - C)\) with shadow price \(\partial V^/\partial b = \lambda^\). The KKT conditions give complementary slackness: \(\lambda^* > 0\) if and only if the constraint binds. Portfolio optimization under risk limits maps directly to this framework, with the shadow price quantifying the cost of each unit of risk budget (Theorem 5).
(3) Robust Bellman. The min-max equation \(V = \max_a \min_\xi [R + \gamma \sum P_\xi V]\) under model uncertainty \(\|\xi\| \leq \varepsilon\) is still a contraction at rate \(\gamma(1+\varepsilon) < 1\), guaranteeing a unique robust fixed point. The price of robustness \(V_{\text{nom}} - V_{\text{rob}} \geq 0\) is monotone in \(\varepsilon\) and vanishes at \(\varepsilon = 0\). This yields model-free option pricing bounds \([V_{\text{low}}, V_{\text{high}}]\) with width \(O(\varepsilon)\) that narrow with data (Theorem 6).
All results are formalized across 14 Lean 4 files (50+ theorems, zero sorry), compiled via lake build with zero errors. To our knowledge, this constitutes the first machine-verified treatment of extended dynamic programming for finance.
Keywords: Bellman equation, spectral decomposition, constrained MDP, robust optimization, option pricing, Lean 4, formal verification
Novelty
The per-mode contraction rate γ|μ_k| for eigenmode-decomposed Bellman equations is a clean observation that unifies spectral value iteration with the COS pricing backward step, though each ingredient (spectral MDP analysis, constrained MDP duality, robust MDP contraction) is individually well-established.