Interval integrability of the running cost along an admissible pair
ProvedBertsekasDP.admissible_cost_integrand_intervalIntegrableoptimal-controlpontryaginvariational-calculus
Let be a continuous running cost on state-control pairs and let be admissible on from the state in the sense of BertsekasCTAdmissibleFrom: has bounded image on and is continuous off a finite set, and is continuous on .
Then for any two times the running cost is interval integrable:
The integrand is continuous off a finite set, hence almost everywhere continuous and measurable, and it is bounded because is compact, is bounded, and is continuous on the resulting compact product. This is the fact that makes the cost functional of an admissible pair a genuine Lebesgue integral, and it is what allows the cost to be split at intermediate times.
Preamble
import Definitions.Def_BertsekasCTModel open Filter open scoped Topology
Formal statement
theorem BertsekasDP.admissible_cost_integrand_intervalIntegrable
{n m : ℕ} (M : BertsekasCTModel n m)
(hg : Continuous (Function.uncurry M.g))
(t₀ : ℝ) (ξ : EuclideanSpace ℝ (Fin n))
(u : ℝ → EuclideanSpace ℝ (Fin m))
(x : ℝ → EuclideanSpace ℝ (Fin n))
(hadm : BertsekasCTAdmissibleFrom M t₀ ξ u x)
(a b : ℝ) (ha : a ∈ Set.Icc t₀ M.T) (hb : b ∈ Set.Icc t₀ M.T) :
IntervalIntegrable (fun t => M.g (x t) (u t)) MeasureTheory.volume a b := by
sorrySource
D. Liberzon, Calculus of Variations and Optimal Control Theory, Sections 4.2.3-4.2.4, equations (4.14)-(4.23), https://liberzon.csl.illinois.edu/teaching/cvoc/node68.html and https://liberzon.csl.illinois.edu/teaching/cvoc/node69.html; adjoint pairing identity (4.32), Section 4.2.8; terminal costs, Section 4.3.1.3, https://liberzon.csl.illinois.edu/teaching/cvoc/node82.html. Fixed-horizon Bolza specialization adapted to the finite-exception admissibility class of BertsekasCTModel (D. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Sections 3.2-3.3.1).