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.
Measurability of integration against a kernel
Statement
Let K be a finite kernel from to , in particular a probability kernel, or a uniformly sigma-finite kernel with the specified exhaustion of the kernel definition. For every nonnegative -measurable function , the function is -measurable, with infinity allowed. For a real product-measurable f, the set is measurable, and its signed integral on D, extended by zero on , is a measurable real function. No assertion here is made for a general kernel lacking a common measurable finite-mass exhaustion.
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
Kernel evaluations are measurable and every section is a measure. Measure kernel and probability kernel.
A lambda-system containing a pi-system contains its generated sigma-algebra. Dynkin's pi-lambda theorem.
Nonnegative measurable functions have explicit increasing simple approximations. Every nonnegative measurable function is the increasing limit of simple measurable functions.
Monotone convergence applies to each section measure. Monotone convergence for the integral.
Measurable functions are closed under defined sums, real scalars, nonnegative restriction and increasing limits. Closure properties of measurable functions used by the integral.
Every section of a product-measurable function is measurable. Every section of a product-measurable function is measurable.
Measurable rectangles generate the product sigma-algebra. The product sigma-algebra and its finite iterates.
Proof
First suppose K finite and write . For a product-measurable set E, its section is measurable, by applying the section theorem to its indicator. Let consist of those E for which is measurable. It contains every rectangle , whose evaluation is , and it contains . If E belongs to this class, then and ; both terms are finite measurable real functions, so the difference is measurable. If E_j are disjoint class members, their sections are disjoint and is an increasing limit of measurable finite sums. Thus this class is a lambda-system. Rectangles form a pi-system, so Dynkin's theorem gives every product-measurable E in the class. The measurable-closure proposition can be used on S equipped with its zero measure; its conclusions concern only Sigma and do not require a preexisting source probability.
For a nonnegative simple product-measurable function with disjoint E_j and finite nonnegative coefficients, its section integral is and is measurable by step 1.1. Choose the prescribed increasing simple approximation on the product. For every s the section theorem and monotone convergence give , so the increasing-limit closure proves measurability. No uniform bound in s was used; only the individual finite masses entered the complement calculation.
Now let be the specified common exhaustion. Define . For each s this is the restriction of a measure, its evaluations are measurable by the kernel hypothesis, and . Apply step 2.1 to K_n. Sectionwise integration against the restriction equals integration of against K(s,·): this holds for indicators by definition, for simple functions by finite sums, and for nonnegative functions by monotone convergence. Since , ; another increasing-limit argument proves the result. If T is empty all these integrals are zero; if S is empty the assertion is vacuous.
For real f its positive and negative parts and absolute value are product-measurable. The proved result makes measurable. Therefore is measurable. On D both part integrals are finite since each is at most . Define on D and zero otherwise, and define J_- similarly. Nonnegative measurable restriction makes both J_± measurable; they are finite everywhere. Their real difference is the requested signed integral on D and zero elsewhere. This never subtracts two infinities. For a zero kernel all integrals vanish and D=S, even if f is unbounded; for f=0 the same holds for every permitted kernel. All approximations and the exhaustion are specified; no AC is used.
Depends on
- Measure kernel and probability kernel
- Dynkin's pi-lambda theorem
- Every nonnegative measurable function is the increasing limit of simple measurable functions
- Monotone convergence for the integral
- Closure properties of measurable functions used by the integral
- Every section of a product-measurable function is measurable
- The product sigma-algebra and its finite iterates
Used by
Dependency tree · two levels
31 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, Probability: Theory and Examples, fifth edition (standard reference, not scraped)
- Varadhan, Probability Theory, Chapter 4 (standard reference, not scraped)