LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Finite response likelihood ratios change measure by cancellation

Statement

Let $Y$ be a finite nonempty response set with a fixed enumeration $(y_{1}, \dots, y_{m})$ , and let $p$ and $q$ be probability mass functions on $Y$ satisfying $p (y) > 0 \Rightarrow q (y) > 0$ . Define $ρ (y) = p (y) / q (y)$ when $q (y) > 0$ and $ρ (y) = 0$ when $q (y) = 0$ . Then, for every real-valued function $f$ on $Y$ ,

$\sum_{j = 1}^{m} q (y_{j}) ρ (y_{j}) f (y_{j}) = \sum_{j = 1}^{m} p (y_{j}) f (y_{j}) .$

In particular, $\sum_{j = 1}^{m} q (y_{j}) ρ (y_{j}) = 1$ . This is a finite response identity; it asserts no change-of-measure result on an arbitrary trajectory space.

Statement references

A probability law assigns total mass one and sums its point masses over finite events.

A finite response policy has normalized masses on its fixed support.

Finite sums are defined by recursion on their upper index.

Facts & Assumptions

Given: The finite response set $Y$ , probability masses $p, q$ , the support inclusion, and a real-valued function $f$ .

[F1]

Probability measures and probability spaces: a probability law is a measure of total mass one; its nonnegative singleton masses on the finite response set sum to one.

[F2]

Finite truncated response spaces, correctness predicates, and verifiers: every prompt has a finite response set and a normalized policy mass function on its fixed support.

[F3]

Finite sums and finite products, by recursion: a sum of $m$ real terms is the recursively defined finite sum over indices $1, \dots, m$ .

Proof

Given: The objects and hypotheses in the Statement.

1.1givenF1F2algebra

For each index $j$ , if $q (y_{j}) = 0$ , support inclusion forces $p (y_{j}) = 0$ and the definition gives $q (y_{j}) ρ (y_{j}) = p (y_{j}) = 0$ . If $q (y_{j}) > 0$ , the quotient is defined and $q (y_{j}) ρ (y_{j}) = p (y_{j})$ . Thus this equality holds for every $j = 1, \dots, m$ .

2.1givenF1F3step 1.1algebra∎

Multiplying the pointwise equality in step 1.1 by $f (y_{j})$ and summing over $j$ using [F3] gives the stated identity. Taking $f (y_{j}) = 1$ gives $\sum_{j = 1}^{m} q (y_{j}) ρ (y_{j}) = \sum_{j = 1}^{m} p (y_{j}) = 1$ . Every operation is a finite sum, so no choice or sigma-finite measure hypothesis is used.

Depends on

Used by

Finite-budget group-relative policy update Algorithm
Reasoning-training evidence and evaluation targets Remark

Dependency tree · two levels

18 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, second-edition draft (standard reference, not scraped)