LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Conditional-independence factorization for integrable outcomes

Statement

Assume AC. Let $(Ω, F, P)$ be a probability space, let $G \subseteq F$ be a sub-sigma-algebra, let $R$ be a random variable taking values in ${0, 1}$ , and let $Y$ be a real integrable random variable. If $R$ and $Y$ are conditionally independent given $G$ , then for every Borel function $φ : R \to R$ such that $φ (Y)$ is integrable, $E [R φ (Y) ∣ G] = E [R ∣ G] E [φ (Y) ∣ G] almost surely .$

Facts & Assumptions

Given: AC, the probability space and sub-sigma-algebra above, $R \in {0, 1}$ , $Y \in L^{1} (P)$ , $R ⊥ ⁣ ⁣ ⁣ ⊥ Y ∣ G$ , and a Borel $φ$ with $Z = φ (Y) \in L^{1} (P)$ .

[F1]

Conditional independence means the conditional product identity for every pair of bounded measurable real functions. (Conditional independence given a sigma-algebra)

[F2]

A conditional-expectation version is measurable, integrable, and satisfies the defining event-integral identity. (Conditional expectation given a sigma algebra)

[F3]

Under AC, conditional expectation is linear and order-preserving, and $E ∣ E [U ∣ G] ∣ \leq E ∣ U ∣$ for every real $U \in L^{1} (P)$ . (Basic algebra and order properties of conditional expectation)

[F4]

Increasing sequences of nonnegative measurable functions pass to the limit under the integral. (Monotone convergence for the integral)

[F5]

For a real measurable $Z$ , integrability means $E ∣ Z ∣ < \infty$ . (Integrable real and complex functions, and their integrals)

[F6]

The expectation of an integrable real random variable is its Lebesgue integral. (Expectation of a nonnegative or integrable random variable)

[A1]

AC is assumed to define conditional independence and guarantee existence of the conditional-expectation classes used here. (The Axiom of Choice, Conditional independence given a sigma-algebra, Basic algebra and order properties of conditional expectation)

Proof

1.1givenA1F1F2

For $m \geq 1$ , put $Z_{m} = \max (- m, \min (Z, m))$ . The functions $z \mapsto \max (- m, \min (φ (z), m))$ and $r \mapsto r$ are bounded and measurable, so [F1] gives $E [R Z_{m} ∣ G] = E [R ∣ G] E [Z_{m} ∣ G]$ , with the conditional-expectation versions interpreted by [F2].

2.1givenF3F4F5F6step 1.1∎

The truncations satisfy $Z_{m} \to Z$ in $L^{1}$ : $∣ Z - Z_{m} ∣ \leq ∣ Z ∣ 1_{{∣ Z ∣ > m}}$ , and [F4] applied to $∣ Z ∣ 1_{{∣ Z ∣ \leq m}} ↑ ∣ Z ∣$ makes the tail integrals tend to zero, using integrability [F5] and expectation as integral [F6]. By [F3], conditional expectation is an $L^{1}$ contraction; since $0 \leq E [R ∣ G] \leq 1$ , both sides of the identity in step 1.1 converge in $L^{1}$ to the corresponding sides for $Z$ . Uniqueness of the $L^{1}$ limit proves the claimed equality.

Source notes

The cited notes define conditional independence only for bounded measurable test functions. The truncation argument above supplies the integrable extension used in this item.

Depends on

Used by

Inverse response-probability weighting identifies the mean under MAR Theorem

Dependency tree · two levels

35 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

Sinho Chewi, Probability Notes for David Aldous, Lecture 9 (standard reference, not scraped)