Verification theorems for stochastic optimal control problems in Hilbert spaces by means of a generalized Dynkin formula

Verification theorems are key results to successfully employ the dynamic programming approach to optimal control problems. In this paper, we introduce a new method to prove verification theorems for infinite dimensional stochastic optimal control problems. The method applies in the case of additively controlled Ornstein–Uhlenbeck processes, when the associated Hamilton–Jacobi–Bellman (HJB) equation admits a mild solution (in the sense of [J. Differential Equations 262 (2017) 3343–3389]). The main methodological novelty of our result relies on the fact that it is not needed to prove, as in previous literature (see, e.g., [Comm. Partial Differential Equations 20 (1995) 775–826]), that the mild solution is a strong solution, that is, a suitable limit of classical solutions of approximating HJB equations. To achieve the goal, we prove a new type of Dynkin formula, which is the key tool for the proof of our main result.