TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Total variation controls expectations of bounded functions

Statement

Let $(E, E)$ be a measurable space, let $P$ and $Q$ be probability measures on it, and let $f : E \to R$ be measurable with $∣ f ∣ \leq M$ pointwise for some finite $M \geq 0$ . With the convention $∥ P - Q ∥_{T V} : = \sup_{A \in E} ∣ P (A) - Q (A) ∣,$ one has $∣ \int f d P - \int f d Q ∣ \leq 2 M ∥ P - Q ∥_{T V} .$ For every measurable $g : E \to R$ with $0 \leq g \leq M$ pointwise, one also has $∣ \int g d P - \int g d Q ∣ \leq M ∥ P - Q ∥_{T V} .$ Both integral differences are zero when $M = 0$ .

Facts & Assumptions

Given: A measurable space $(E, E)$ , probability measures $P, Q$ , and measurable real functions $f, g$ satisfying $∣ f ∣ \leq M < \infty$ and $0 \leq g \leq M$ .

[F1]

A probability measure has total mass one. Probability measures and probability spaces

[F2]

Total variation here is the event supremum $\sup_{A \in E} ∣ P (A) - Q (A) ∣$ and has no half-factor. Total variation distance for probability laws

[F3]

On nonnegative simple functions, the nonnegative Lebesgue integral agrees with the simple integral. The nonnegative integral agrees with the simple integral on simple functions

[F4]

The simple integral is the sum of the coefficients times the measures of the level sets; in particular, an indicator integrates to the measure of its set. The integral of a nonnegative simple function

[F5]

The nonnegative integral is additive, monotone, and nonnegatively homogeneous. Additivity of the nonnegative Lebesgue integral Monotonicity and nonnegative homogeneity of the nonnegative integral

[F6]

A real measurable function is integrable when its absolute value has finite nonnegative integral; the integral is linear on integrable functions. Integrable real and complex functions, and their integrals The Lebesgue integral is linear on $L^{1} (μ)$

[F7]

For every $η > 0$ there is an integer $n \geq 1$ with $1 / n < η$ . For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$

Proof

Given: The hypotheses in the Statement.

1.1givenconstruct

If $M = 0$ , then $f = 0$ and $g = 0$ pointwise, so both claims hold. To prove the nonnegative claim for an arbitrary finite bound $L > 0$ , let $w : E \to R$ be measurable with $0 \leq w \leq L$ , fix an integer $n \geq 1$ , put $Δ = L / n$ , and define $A_{k} = {x : w (x) \geq k Δ}$ for $1 \leq k \leq n$ and $s_{n} = Δ \sum_{k = 1}^{n} 1_{A_{k}}$ . The sets are measurable, $s_{n}$ is nonnegative simple, and $0 \leq w - s_{n} \leq Δ$ pointwise.

2.1F1F2F3F4F5step 1.1algebra

By [F3]–[F5], $\int s_{n} d P = Δ \sum_{k = 1}^{n} P (A_{k})$ and likewise for $Q$ , so $∣ \int s_{n} d P - \int s_{n} d Q ∣ \leq n Δ ∥ P - Q ∥_{T V} = L ∥ P - Q ∥_{T V}$ . Also $0 \leq \int (w - s_{n}) d P \leq Δ$ and $0 \leq \int (w - s_{n}) d Q \leq Δ$ , because $w - s_{n} \leq Δ$ and both measures have mass one. The triangle inequality therefore gives $∣ \int w d P - \int w d Q ∣ \leq L ∥ P - Q ∥_{T V} + 2 L / n$ .

3.1F7step 2.1algebra

Given any $η > 0$ , choose $n$ by [F7] with $1 / n < η / (2 L)$ . The estimate in step 2.1 then gives $∣ \int w d P - \int w d Q ∣ < L ∥ P - Q ∥_{T V} + η$ . If the bound by $L ∥ P - Q ∥_{T V}$ failed, choosing $η$ to be half the positive excess would contradict this inequality. Taking $w = g$ and $L = M$ proves the stated nonnegative case when $M > 0$ .

4.1F1F3F4F5F6step 3.1algebra∎

For the signed case with $M > 0$ , let $h = f + M$ . Then $h$ is measurable and $0 \leq h \leq 2 M$ , so step 3.1 with $w = h$ and $L = 2 M$ gives $∣ \int h d P - \int h d Q ∣ \leq 2 M ∥ P - Q ∥_{T V}$ . Also $∣ f ∣ \leq M$ , so [F1], [F3]–[F5] give $\int ∣ f ∣ d P \leq M$ and $\int ∣ f ∣ d Q \leq M$ ; hence $f$ is integrable under both measures by [F6]. The constant $M$ has integral $M$ under each probability measure, so linearity [F6] gives $\int f d P - \int f d Q = \int h d P - \int h d Q$ . This proves the signed case.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Alison L. Gibbs and Francis E. Su, On Choosing and Bounding Probability Metrics, International Statistical Review 70(3), 419–435 (2002) (standard reference, not scraped)
David A. Levin, Yuval Peres, and Elizabeth L. Wilmer, Markov Chains and Mixing Times, 2nd ed. (standard reference, not scraped)