OLFC beats open-loop control (Prop. 6.2.1)

Proved

BertsekasDP.olfc_performance

by Shuze Chen · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

olfcopen-loopcontrol

Proposition 6.2.1 (the open-loop feedback controller uses measurements advantageously). Consider the basic stochastic model with state-independent control constraint sets, in the perfect state information case. The open-loop feedback controller (OLFC) $\bar\pi$ acts as follows: at stage $k$ in state $x$ , it solves the open-loop problem over the remaining horizon starting from $x$ — optimizing over control sequences, as if no further measurements were to be received — and applies the first control of an optimal such sequence. Then for every initial state $x_0$ ,

J_{\bar\pi}(x_0) \;\le\; J_u(x_0) \qquad \text{for every admissible open-loop control sequence } u = (u_0, \dots, u_{N-1}).

That is, the closed-loop cost of the OLFC is at most the cost of the best fixed control sequence.

The point is that a suboptimal scheme should at least not waste the information it receives. The OLFC selects each control as if the future were unobservable, yet because it re-optimizes at every stage from the state actually reached, it dominates every policy that ignores observations altogether. This guarantee is what distinguishes it from the certainty equivalent controller, which, as the source notes, can be strictly worse than the optimal open-loop policy.

Formalization Note The constraint sets are assumed independent of the state, matching the open-loop framework of §6.2 in which a single sequence must be feasible along all trajectories. The OLFC is characterized by a hypothesis — at each stage and state there exists an optimal admissible sequence whose first control the policy plays — rather than constructed, so the statement is about any policy with that property. The perfect-information case is the one formalized here; the source's general version additionally propagates the conditional state distribution.

Preamble

import Mathlib
import Definitions.Def_BertsekasDPModel
import Definitions.Def_BertsekasDPOpenLoopCost

Formal statement

namespace BertsekasDP

theorem olfc_performance {S C W : Type} [Fintype W]
    (M : BertsekasDPModel S C W)
    (hUconst : ∀ k x x', M.U k x = M.U k x')
    (π : ℕ → S → C)
    (holfc : ∀ k, k < M.N → ∀ x, ∃ useq : ℕ → C,
      (∀ i, k ≤ i → i < M.N → useq i ∈ M.U i x) ∧
      π k x = useq k ∧
      (∀ useq' : ℕ → C, (∀ i, k ≤ i → i < M.N → useq' i ∈ M.U i x) →
        BertsekasDPOpenLoopCost M useq (M.N - k) x ≤
          BertsekasDPOpenLoopCost M useq' (M.N - k) x)) :
    ∀ (x₀ : S) (useq₀ : ℕ → C), (∀ i, i < M.N → useq₀ i ∈ M.U i x₀) →
      BertsekasDPPolicyCost M π M.N x₀ ≤
        BertsekasDPOpenLoopCost M useq₀ M.N x₀ := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 6.2.1 (perfect-information form)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Same setting: types $S, C, W$ with $W$ finite, $M$ a term of the not-provided structure BertsekasDPModel, the not-provided opaque policy-cost $J_\pi(m,x)$ , and the open-loop cost $J^{u_\bullet}_m(x)$ of BertsekasDPOpenLoopCost as unfolded above (steps indexed by truncated subtraction from $N$ ; terminal value $g_N$ ). Hypotheses:

(hUconst) for every stage $k$ and all states $x, x'$ : $U_k(x) = U_k(x')$ — the constraint set at each stage does not depend on the state;
$\pi : \mathbb{N} \to S \to C$ $π : N \to S \to C$ is a policy such that: (holfc) for every $k < N$ $k < N$ and every state $x$ $x$ , there exists a control sequence $u_\bullet : \mathbb{N} \to C$ $u_{∙} : N \to C$ with
1. $u_\bullet(i) \in U_i(x)$ for every $i$ with $k \le i < N$ (admissibility, checked against the constraint sets at the state $x$ , and only on stages $k, \dots, N-1$ ; values of $u_\bullet$ outside that range are unconstrained),
2. $\pi_k(x) = u_\bullet(k)$ (the policy plays the first control of that sequence), and
3. for every competing sequence $u'_\bullet : \mathbb{N} \to C$ satisfying the same admissibility condition (1),

J^{u_\bullet}_{N-k}(x) \;\le\; J^{u'_\bullet}_{N-k}(x),

i.e. $u_\bullet$ minimizes the $(N-k)$ -step open-loop cost from $x$ among all sequences admissible at $x$ on stages $k,\dots,N-1$ . (Since $k \le N$ here, $N-k$ involves no truncation, and unfolding the recursion these $N-k$ steps use exactly the stage data $k, k+1, \dots, N-1$ followed by the terminal cost $g_N$ .)

Conclusion: for every initial state $x_0$ and every control sequence $u^0_\bullet : \mathbb{N} \to C$ satisfying $u^0_\bullet(i) \in U_i(x_0)$ for all $i < N$ ,

J_\pi(N, x_0) \;\le\; J^{u^0_\bullet}_N(x_0),

i.e. the (opaque) policy cost of $\pi$ over $N$ steps from $x_0$ is at most the $N$ -step open-loop cost of any admissible-at- $x_0$ control sequence. When $N = 0$ both hypotheses (holfc) and the admissibility premise are vacuous and the conclusion compares two applications at step count $0$ . The proof is left as sorry.

Human review

Endorsed by Community (Bot) · Sep 11, 2026
Endorsed by Shuze Chen · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph