LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Expected discounted policy value is a fixed point of its Bellman operator

Statement

For a finite MDP, a discount $0 \leq γ < 1$ , and any stationary Markov policy $π$ , the expected discounted state value defined from each initial state satisfies

$T^{π} V^{π} = V^{π} .$

If $S = \emptyset$ , this is the equality of the unique empty functions and no choice axiom is needed. If $S \neq \emptyset$ , assume the Axiom of Choice for the path-law definition of $V^{π}$ .

Statement references

Sutton and Barto, Reinforcement Learning: An Introduction.

Kaelbling, Littman, and Cassandra, Brown Technical Report CS-96-08.

Choice for the nonempty-state chain construction.

Facts & Assumptions

Given: A finite MDP, $0 \leq γ < 1$ , a stationary policy $π$ , and the Axiom of Choice.

[A1]

The Axiom of Choice: Choice is assumed for the path-space construction used to define the start-state expectation.

[F1]

Discounted returns and policy values in a finite MDP: $V^{π} (s)$ is the expectation of the absolutely convergent discounted return under the policy-induced chain started at $(s, 0)$ ; each return is bounded by $M / (1 - γ)$ .

[F2]

A finite MDP and stationary policy generate a reward-state Markov chain: the chain has the homogeneous kernel obtained by mixing the MDP's joint reward-transition law with $π$ , and its finite-prefix laws are the iterated kernel products.

[F3]

Policy Bellman operator: $(T^{π} V) (s) = \sum_{a} π (a ∣ s) \sum_{s^{'}, ρ} p (s^{'}, ρ ∣ s, a) [ρ + γ V (s^{'})]$ .

[F4]

Absolute convergence and tail bound for bounded discounted rewards: each finite partial discounted return is bounded in absolute value by $M / (1 - γ)$ and converges pointwise to the full return.

[F5]

Probability measures and probability spaces and Monotonicity and nonnegative homogeneity of the nonnegative integral: a constant $B \geq 0$ on a probability space is integrable with integral $B$ .

[F6]

Dominated convergence: measurable returns converging pointwise under one integrable majorant have expectations converging to the expectation of their limit.

[F7]

Algebra of limits: sums, scalar multiples, products and quotients: limits commute with finite sums and multiplication by fixed real scalars.

[F8]

Convergence depends only on the tail: the shifted sequence $(V_{N + 1}^{π})_{N \geq 0}$ has the same limit as $(V_{N}^{π})_{N \geq 0}$ .

[F9]

A sequence has at most one limit: a real sequence has at most one limit.

Proof

1.1givenA1F1F2F4F5construct

If $S = \emptyset$ , the claimed equality is between the unique empty functions. Otherwise assume $S \neq \emptyset$ . For every $t \in S$ and $N \geq 0$ , on the path law started at $(t, 0)$ put $G_{N, t} = \sum_{j = 0}^{N - 1} γ^{j} R_{j + 1}, V_{N}^{π} (t) = E_{π, t} [G_{N, t}] .$ Each $G_{N, t}$ is a finite sum of measurable reward coordinates; [F4] bounds its absolute value by $B = M / (1 - γ)$ , and [F5] gives $\int ∣ G_{N, t} ∣ \leq B < \infty$ . Thus the expectations are finite, and the empty sum gives $V_{0}^{π} (t) = 0$ .

1.2givenF1F2F3algebra

The chain's finite-prefix law [F2] gives $V_{N + 1}^{π} (s) = \sum_{a \in A (s)} π (a ∣ s) \sum_{s^{'} \in S, ρ \in R} p (s^{'}, ρ ∣ s, a) [ρ + γ V_{N}^{π} (s^{'})] .$ Indeed the first transition from $(s, 0)$ has mass $\sum_{a} π (a ∣ s) p (s^{'}, ρ ∣ s, a)$ ; after that transition the remaining $N$ -step law depends on $s^{'}$ but not on the reward coordinate, since $K_{π} ((s^{'}, ρ), \cdot) = K_{π} ((s^{'}, 0), \cdot)$ . Expanding the finite sums and using $r (s, a) = \sum_{s^{'}, ρ} ρ p (s^{'}, ρ ∣ s, a)$ and $P (s^{'} ∣ s, a) = \sum_{ρ} p (s^{'}, ρ ∣ s, a)$ shows the right side is $(T^{π} V_{N}^{π}) (s)$ .

2.1step 1.1A1F1F2F4F5F6

For each $s \in S$ , [F4] gives $G_{N, s} \to G_{0}$ pointwise and $∣ G_{N, s} ∣ \leq M / (1 - γ)$ . The constant majorant is integrable by [F5] on the path law from [F2]. Dominated convergence [F6] therefore gives $V_{N}^{π} (s) \to V^{π} (s)$ for every $s \in S$ .

3.1step 1.2step 2.1F3F7F8F9algebra∎

Fix $s \in S$ . In step 1.2 the left side $V_{N + 1}^{π} (s)$ has the same limit $V^{π} (s)$ as $V_{N}^{π} (s)$ by [F8]. By step 2.1 each $V_{N}^{π} (s^{'})$ converges to $V^{π} (s^{'})$ ; [F7] passes these limits through the finite sum on the right, whose limit is $\sum_{a \in A (s)} π (a ∣ s) \sum_{s^{'}, ρ} p (s^{'}, ρ ∣ s, a) [ρ + γ V^{π} (s^{'})] = (T^{π} V^{π}) (s)$ by [F3]. Uniqueness [F9] gives $V^{π} (s) = (T^{π} V^{π}) (s)$ . Since $s$ was arbitrary, $T^{π} V^{π} = V^{π}$ .

Depends on

Used by

Dependency tree · two levels

77 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)
Leslie Pack Kaelbling, Michael L. Littman, and Anthony R. Cassandra, Planning and Acting in Partially Observable Stochastic Domains, Brown CS-96-08 (standard reference, not scraped)