LemmaStatement: AI-adaptedProof: 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.

Integration against a Dirac measure evaluates at its point

Statement

Let $A$ be a sigma-algebra on a set $X$ , let $x_{0} \in X$ , and let $δ_{x_{0}}$ be the Dirac probability measure on $(X, A)$ . For every nonnegative $A$ -measurable $f : X \to [0, + \infty]$ , $\int_{X} f d δ_{x_{0}} = f (x_{0}) .$

Facts & Assumptions

Given: A measurable space, a point $x_{0}$ in it, its Dirac measure, and a nonnegative measurable function $f$ .

[F1]

$δ_{x_{0}} (A) = 1$ if $x_{0} \in A$ and $0$ otherwise, and this set function is a probability measure on $(X, A)$ . (The Dirac set function at a point, A Dirac set function is a probability measure)

[F2]

A nonnegative simple function has a finite representation by disjoint measurable sets, and its simple integral is the sum of its values times the set measures. (Nonnegative simple measurable functions, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions)

[F3]

Every nonnegative measurable function is the pointwise increasing limit of nonnegative simple functions. (Every nonnegative measurable function is the increasing limit of simple measurable functions)

[F4]

Increasing limits pass through the nonnegative Lebesgue integral. (Monotone convergence for the integral)

Proof

technique · direct

1.1F1F2

If $s = \sum_{j = 1}^{m} c_{j} 1_{A_{j}}$ is a nonnegative simple function with pairwise disjoint $A_{j} \in A$ , then [F1] and [F2] give $\int s d δ_{x_{0}} = \sum_{j} c_{j} δ_{x_{0}} (A_{j}) = \sum_{j} c_{j} 1_{A_{j}} (x_{0}) = s (x_{0})$ .

2.1F3F4step 1.1choose∎

Choose the increasing simple approximation $s_{n} ↑ f$ from [F3]. By [F4] and step 1.1, $\int f d δ_{x_{0}} = \lim_{n} \int s_{n} d δ_{x_{0}} = \lim_{n} s_{n} (x_{0}) = f (x_{0})$ , including when the value is $+ \infty$ .

Depends on

Used by

Bias and mean squared error Definition
The Metropolized Hamiltonian chain preserves its target Theorem

Dependency tree · two levels

23 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

Sheldon Axler, Measure, Integration & Real Analysis, Example 2.55 (standard reference, not scraped)
Terence Tao, An Introduction to Measure Theory, Example 1.4.29 (standard reference, not scraped)