LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Discounted occupancy change is bounded by average policy TV

Statement

Let a finite discounted CMDP and two stationary policies $π, π^{'}$ be given, with normalized discounted occupancies $d^{π}, d^{π^{'}}$ . Define

${TV}_{s} (π^{'}, π) : = \frac{1}{2} \sum_{a \in A (s)} ∣ π^{'} (a ∣ s) - π (a ∣ s) ∣$

and $∥ x ∥_{1} : = \sum_{s \in S} ∣ x (s) ∣$ for a state vector. Then

$∥ d^{π^{'}} - d^{π} ∥_{1} \leq \frac{2 γ}{1 - γ} \sum_{s \in S} d^{π} (s) {TV}_{s} (π^{'}, π) .$

Statement references

A finite CMDP has finite states and actions, a normalized joint transition law, and stationary policies.

Normalized discounted state occupancy: The normalized occupancy is $(1 - γ)$ times the discounted sum of state-mass vectors.

Each state-mass vector and the resulting occupancy are probability distributions.

Achiam et al., Constrained Policy Optimization, supplementary material, Appendix 10.1.

Altman, Constrained Markov Decision Processes, Chapter 3 §3.1.

Facts & Assumptions

Given: A finite CMDP, $0 \leq γ < 1$ , stationary policies $π, π^{'}$ , and their state-mass vectors and normalized discounted occupancies.

[F1]

Finite discounted constrained Markov decision process: $S$ and each $A (s)$ are finite, $p (s^{'}, ρ ∣ s, a)$ is a normalized joint law, $P (s^{'} ∣ s, a) : = \sum_{ρ} p (s^{'}, ρ ∣ s, a)$ is a probability distribution, and $π (a ∣ s)$ is a probability distribution over $A (s)$ .

[F2]

Normalized discounted state occupancy: $d^{σ} = (1 - γ) \sum_{t \geq 0} γ^{t} μ_{t}^{σ}$ and the column transition matrix is $K_{σ} (s^{'}, s) = \sum_{a, ρ} σ (a ∣ s) p (s^{'}, ρ ∣ s, a)$ .

[F3]

Normalized discounted occupancy is a probability distribution: every $μ_{t}^{σ}$ and $d^{σ}$ is a probability distribution.

[F4]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: $\sum_{t = 0}^{\infty} γ^{t} = 1 / (1 - γ)$ for $0 \leq γ < 1$ .

[F5]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : $γ^{n} \to 0$ for $0 \leq γ < 1$ .

Proof

1.1F1F4F5givenalgebra

For $σ \in {π, π^{'}}$ , every entry of $K_{σ}$ is nonnegative and each column sums to one by [F1]. Thus $K_{σ}^{t}$ is column-stochastic for every $t$ , and its induced matrix $1$ -norm $∥ A ∥_{1} : = \max_{s} \sum_{s^{'}} ∣ A (s^{'}, s) ∣$ is one. Every entry of $K_{σ}^{t}$ lies in $[0, 1]$ , so each of the finitely many coordinate series $\sum_{t = 0}^{\infty} γ^{t} (K_{σ}^{t}) (s^{'}, s)$ converges by comparison with [F4]; their limits give convergence of the matrix partial sums in this finite-dimensional norm. The matrix series $G_{σ} : = \sum_{t = 0}^{\infty} γ^{t} K_{σ}^{t}$ therefore exists; its finite partial sums satisfy $(I - γ K_{σ}) \sum_{t = 0}^{N} γ^{t} K_{σ}^{t} = I - γ^{N + 1} K_{σ}^{N + 1}$ , whose remainder norm tends to zero by [F5]. The same identity with multiplication on the other side shows $G_{σ} = (I - γ K_{σ})^{- 1}$ .

1.2F1F3algebra

By [F1], for each coordinate $s^{'}$ of $(K_{π^{'}} - K_{π}) d^{π}$ , the triangle inequality gives $\sum_{s^{'}} ∣ ((K_{π^{'}} - K_{π}) d^{π}) (s^{'}) ∣ \leq \sum_{s, a, s^{'}} d^{π} (s) ∣ π^{'} (a ∣ s) - π (a ∣ s) ∣ P (s^{'} ∣ s, a) = 2 \sum_{s} d^{π} (s) {TV}_{s} (π^{'}, π)$ , because $\sum_{s^{'}} P (s^{'} ∣ s, a) = 1$ .

2.1F1F2step 1.1algebra

The recurrence in [F1] and the matrix definition in [F2] give $μ_{t}^{σ} = K_{σ}^{t} μ$ , hence $d^{σ} = (1 - γ) G_{σ} μ$ . The inverse identity $G_{π^{'}} - G_{π} = G_{π^{'}} [(I - γ K_{π}) - (I - γ K_{π^{'}})] G_{π}$ therefore yields $d^{π^{'}} - d^{π} = γ G_{π^{'}} (K_{π^{'}} - K_{π}) d^{π}$ .

3.1F4step 2.1step 1.2algebra∎

Since $∥ G_{π^{'}} ∥_{1} \leq \sum_{t \geq 0} γ^{t} = 1 / (1 - γ)$ by [F4] and column-stochasticity, combine step 2.1 with step 1.2 to obtain the claimed $1$ -norm bound.

Depends on

Used by

Policy performance bound by average divergence Theorem

Dependency tree · two levels

32 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

Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel, Constrained Policy Optimization, supplementary material (standard reference, not scraped)
Eitan Altman, Constrained Markov Decision Processes (standard reference, not scraped)