ExampleConstruction: AI-adaptedVerification: 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.

Empirical laws of a finite valued iid sample

Example

For IID samples with law $μ = \sum_{j = 1}^{m} p_{j} δ_{a_{j}}$ on distinct points $a_{1}, \dots, a_{m} \in R^{d}$ , where $p_{j} \geq 0$ and $\sum_{j} p_{j} = 1$ , the empirical laws converge weakly almost surely. On outcomes whose samples all lie in this finite set, weak convergence is equivalent to convergence of all atom frequencies to $p_{j}$ .

Facts & Assumptions

[F1]

Empirical measures of iid euclidean samples converge weakly: For IID $R^{d}$ -valued samples $(X_{i})$ with common law $μ$ and finite $d \geq 1$ , the empirical probabilities ${\hat{μ}}_{n} = n^{- 1} \sum_{i = 1}^{n} δ_{X_{i}}$ converge weakly to $μ$ almost surely on one common event.

[F2]

Finite and countable subadditivity of measures: Let $μ$ be a measure and let $(E_{k})_{k \in N}$ be measurable. Then

$μ (⋃_{k \in N} E_{k}) \leq \sum_{k = 0}^{\infty} μ (E_{k}) .$

For every $m \in N$ one also has

$μ (⋃_{k < m} E_{k}) \leq \sum_{k < m} μ (E_{k}),$

including $m = 0$ , where both sides are $0$ .

Verification

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1F1F2

Apply F2 to the union of the sample-outside-support events. By F1, the empirical laws converge weakly almost surely. Also all samples lie in the finite set on a conull event, since each outside event has probability zero and there are countably many coordinates.

1.2givenalgebra

On such an outcome put $q_{n, j} = n^{- 1} # {i \leq n : X_{i} = a_{j}}$ . If each $q_{n, j} \to p_{j}$ , then for bounded continuous f, $\int f d {\hat{μ}}_{n} = \sum_{j} q_{n, j} f (a_{j}) \to \sum_{j} p_{j} f (a_{j}) = \int f d μ$ , proving weak convergence.

2.1givenalgebra∎

Conversely, for $m \geq 2$ put $r_{j} = \frac{1}{2} \min_{l \neq j} ∥ a_{j} - a_{l} ∥ > 0$ and $f_{j} (x) = \max (0, 1 - ∥ x - a_{j} ∥ / r_{j})$ . This bounded continuous test is one at $a_{j}$ and zero at every other $a_{l}$ . Its empirical integral is $q_{n, j}$ and its $μ$ integral is $p_{j}$ , so weak convergence implies $q_{n, j} \to p_{j}$ . If $m = 1$ , both frequencies are identically one and the constant test suffices.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Durrett, §§2.4–2.5, pp. 76–87 (standard reference, not scraped)