ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-10

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.

Strong law for empirical indicator averages

Example

For IID random elements $(X_{n})$ and a fixed measurable A, $n^{- 1} \sum_{k \leq n} 1_{A} (X_{k}) \to P (X_{1} \in A)$ almost surely. A single conull event works for any specified countable class of sets A.

Facts & Assumptions

[F1]

Measurable coordinatewise functions preserve independence: Let $(X_{i})_{i \in I}$ be an independent family of random elements $X_{i} : (Ω, F, P) \to (S_{i}, Σ_{i})$ . For each $i$ , let $g_{i} : (S_{i}, Σ_{i}) \to (T_{i}, T_{i})$ be measurable. Then the family $(g_{i} \circ X_{i})_{i \in I}$ is independent.

[F2]

The expectation of an indicator is the probability of the event: Let $(Ω, F, P)$ be a probability space and let $A \in F$ . Then the indicator $1_{A}$ satisfies $E [1_{A}] = P (A) .$

[F3]

Kolmogorov iid l1 strong law: For IID real $(X_{n})_{n \geq 1}$ with $E ∣ X_{1} ∣ < \infty$ , $S_{n} / n \to μ = E X_{1}$ almost surely.

[F4]

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.1

The measurable maps $x \mapsto 1_{A} (x)$ take values in {0,1}. F1 preserves the IID property, and F2 computes their expectation as $p_{A} = P (X_{1} \in A)$ ; their absolute expectations are at most one.

F1F2

2.1

F3 applied to step 1.1 gives the fixed-set limit. For a specified countable class, let N_A be the failure event for that limit. F4 gives $P (⋃_{A} N_{A}) \leq \sum_{A} 0 = 0$ . Outside this union every stated frequency converges simultaneously.

F3F4step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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)