DefinitionDefinition: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pending

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Optimal action-value Bellman operator

Definition

Let a finite MDP have nonempty finite state set $S$ and let $0 \leq γ < 1$ . Write $D = {(s, a) : s \in S, a \in A (s)}$ and $R^{D}$ for the real functions on $D$ . The optimal action-value Bellman operator $H : R^{D} \to R^{D}$ is

(H Q) (s, a) = \sum_{s^{'} \in S} \sum_{ρ \in R} p (s^{'}, ρ ∣ s, a) [ρ + γ \max_{b \in A (s^{'})} Q (s^{'}, b)] ((s, a) \in D) .

Each maximum is attained because every $A (s^{'})$ is finite and nonempty.

Definition references

The finite state set, admissible state-action pairs, and joint reward-transition masses.

A maximum is an attained upper bound belonging to the set.

Every nonempty finite set of real numbers has an attained maximum.

Sutton and Barto, Reinforcement Learning: An Introduction.

Yang, Optimal Control and Reinforcement Learning, Chapter 2.

Facts & Assumptions

Given: A finite MDP with nonempty finite state set $S$ , nonempty finite action sets $A (s)$ , finite reward set $R$ , joint masses $p (s^{'}, ρ ∣ s, a)$ , and $0 \leq γ < 1$ .

[F1]

Finite Markov decision process with joint reward-transition law: every $A (s^{'})$ is nonempty and finite, $D$ is the set of admissible pairs, and each $p (\cdot, \cdot ∣ s, a)$ is a probability mass on the finite set $S \times R$ .

[F2]

Finite, countably infinite, countable, uncountable and Every nonzero natural number is a successor: a nonempty finite action set is in bijection with a nonzero natural number, and every nonzero natural is the successor $σ (n)$ of a natural $n$ ; thus its actions can be listed as $a_{0}, \dots, a_{n}$ .

[F3]

Every nonempty finite set of reals has a maximum and a minimum: for every natural $n$ and real list $u_{0}, \dots, u_{n}$ , the set ${u_{0}, \dots, u_{n}}$ has an attained maximum and minimum.

[F4]

Maximum and minimum of a set: a maximum of a real set belongs to that set and is an upper bound for every member; it is unique when it exists.

[F5]

The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form: a real-valued function on a finite index set has a well-defined finite sum.

Verification

Given: The finite MDP, its nonempty finite state-action domain, the discount, and the candidate formula for $H$ in the Definition.

1.1givenF1F2F3construct

Fix $s^{'} \in S$ . By [F1] and [F2], choose a natural $n$ and a bijection $ϕ : σ (n) \to A (s^{'})$ . The list $u_{j} = Q (s^{'}, ϕ (j))$ for $j \in σ (n)$ has an attained maximum $m$ by [F3]. Every action $b \in A (s^{'})$ equals $ϕ (j)$ for some $j$ , so $Q (s^{'}, b) \leq m$ , and the maximum value $m$ is attained by at least one such action.

2.1step 1.1F4algebra

The maximum value in step 1.1 depends only on the set ${Q (s^{'}, b) : b \in A (s^{'})}$ : it belongs to that set and bounds every member. Uniqueness in [F4] therefore makes it independent of the enumeration $ϕ$ . Hence $\max_{b \in A (s^{'})} Q (s^{'}, b)$ is well-defined.

3.1givenF1F5step 2.1algebra∎

For each $(s, a) \in D$ , the bracketed term in the Definition is real by step 2.1, and $S \times R$ is finite by [F1]. The finite sum supplied by [F5] is therefore a real number. Thus the displayed formula assigns one real value to every coordinate in $D$ and defines a map $H : R^{D} \to R^{D}$ .

Depends on

Used by

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed. (standard reference, not scraped)
Han-Dong Yang, Optimal Control and Reinforcement Learning, Chapter 2: Value-based Reinforcement Learning (standard reference, not scraped)