Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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 (S,Σ) to (T,T), in particular a probability kernel, or a uniformly sigma-finite kernel with the specified exhaustion of the kernel definition. For every nonnegative ΣT-measurable function f:S×T[0,], the function If(s)=Tf(s,t)K(s,dt) is Σ-measurable, with infinity allowed. For a real product-measurable f, the set D={s:If(s)<} is measurable, and its signed integral on D, extended by zero on SD, 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.

[F1]

Kernel evaluations are measurable and every section is a measure. Measure kernel and probability kernel.

[F2]

A lambda-system containing a pi-system contains its generated sigma-algebra. Dynkin's pi-lambda theorem.

[F3]

Nonnegative measurable functions have explicit increasing simple approximations. Every nonnegative measurable function is the increasing limit of simple measurable functions.

[F4]

Monotone convergence applies to each section measure. Monotone convergence for the integral.

[F5]

Measurable functions are closed under defined sums, real scalars, nonnegative restriction and increasing limits. Closure properties of measurable functions used by the integral.

[F6]

Every section of a product-measurable function is measurable. Every section of a product-measurable function is measurable.

[F7]

Measurable rectangles generate the product sigma-algebra. The product sigma-algebra and its finite iterates.

Proof

technique · direct
1.1

First suppose K finite and write m(s)=K(s,T)<. For a product-measurable set E, its section Es is measurable, by applying the section theorem to its indicator. Let D consist of those E for which sK(s,Es) is measurable. It contains every rectangle A×B, whose evaluation is 1A(s)K(s,B), and it contains S×T. If E belongs to this class, then (Ec)s=TEs and K(s,(Ec)s)=m(s)K(s,Es); both terms are finite measurable real functions, so the difference is measurable. If E_j are disjoint class members, their sections are disjoint and K(s,(jEj)s)=jK(s,(Ej)s) 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.

F1F2F5F6F7
2.1

For a nonnegative simple product-measurable function g=j=1raj1Ej with disjoint E_j and finite nonnegative coefficients, its section integral is jajK(s,(Ej)s) and is measurable by step 1.1. Choose the prescribed increasing simple approximation gnf on the product. For every s the section theorem and monotone convergence give If(s)=limnIgn(s), so the increasing-limit closure proves measurability. No uniform bound in s was used; only the individual finite masses entered the complement calculation.

step 1.1F3F4F5F6
3.1

Now let (Tn) be the specified common exhaustion. Define Kn(s,A)=K(s,ATn). For each s this is the restriction of a measure, its evaluations are measurable by the kernel hypothesis, and Kn(s,T)=K(s,Tn)<. Apply step 2.1 to K_n. Sectionwise integration against the restriction equals integration of f(s,)1Tn against K(s,·): this holds for indicators by definition, for simple functions by finite sums, and for nonnegative functions by monotone convergence. Since TnT, If(s)=limnf(s,t)Kn(s,dt); another increasing-limit argument proves the result. If T is empty all these integrals are zero; if S is empty the assertion is vacuous.

step 2.1F1F3F4F5
4.1

For real f its positive and negative parts and absolute value are product-measurable. The proved result makes If+,If,If measurable. Therefore D=n1{If<n} is measurable. On D both part integrals are finite since each is at most If. Define J+(s)=If+(s) 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.

step 2.1step 3.1F5

Depends on

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