LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Continuous functions determine Borel probabilities on compact metric spaces

Statement

Let $K$ be a nonempty compact metric space. If Borel probability measures $μ$ and $ν$ satisfy

$\int_{K} f d μ = \int_{K} f d ν for every f \in C (K, R),$

then $μ = ν$ .

Facts & Assumptions

Given: The compact metric space and Borel probabilities in the Statement.

[F1]

Dominated convergence applies to bounded pointwise-convergent measurable functions (Dominated convergence).

[F2]

Two finite measures of equal total mass which agree on a generating pi-system agree on its generated sigma-algebra (Finite measures agreeing on a generating pi-system and on the whole space are equal).

[F3]

Distance to a nonempty subset is a real-valued $1$ -Lipschitz function, and a nonempty closed set is exactly its zero-distance set ( $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset).

Proof

technique · direct approximation of closed-set indicators

1.1

Let $F \subseteq K$ be closed and nonempty. By [F3], its distance function is continuous, vanishes on $F$ , and is strictly positive off $F$ . For $m \geq 1$ , set $ϕ_{m} (x) = \max {0, 1 - m d (x, F)} .$ Then $0 \leq ϕ_{m} \leq 1$ , every $ϕ_{m}$ is continuous, and $ϕ_{m} ↓ 1_{F}$ pointwise.

F3algebra

2.1

The assumed continuous-test identity applies to each $ϕ_{m}$ . Dominated convergence for each probability measure gives $μ (F) = \lim_{m} \int ϕ_{m} d μ = \lim_{m} \int ϕ_{m} d ν = ν (F) .$ For $F = \emptyset$ the same equality is immediate.

F1step 1.1

3.1

Closed subsets of $K$ form a pi-system containing $K$ , and their complements are the open sets, so they generate the Borel sigma-algebra. The two probabilities have equal total mass one and agree on every closed set by step 2.1. Applying [F2] proves $μ = ν$ .

F2step 2.1∎

Depends on

Used by

Unique ergodicity is equivalent to uniform ergodic averages Theorem

Dependency tree · two levels

39 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

Charles Walkden, Ergodic Theory lecture notes (standard reference, not scraped)