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

Conditional fatou and dominated convergence

Statement

Assume AC. For nonnegative measurable $X_{n}$ , $E [{lim inf}_{n} X_{n} ∣ G] \leq {lim inf}_{n} E [X_{n} ∣ G]$ almost surely, in the extended sense. If real-valued measurable $X_{n}$ and $X$ satisfy $X_{n} \to X$ almost surely and $∣ X_{n} ∣ \leq W$ almost surely for one nonnegative $W \in L^{1} (P)$ , then $E [X_{n} ∣ G] \to E [X ∣ G]$ almost surely and in $L^{1}$ .

Facts & Assumptions

Given: AC and nonnegative measurable $X_{n}$ ; separately real-valued measurable $X_{n}$ and $X$ such that $X_{n} \to X$ almost surely and $∣ X_{n} ∣ \leq W$ for one nonnegative integrable $W$ .

[F1]

Extended conditional expectation preserves order and increasing limits. (Conditional monotone convergence)

[F2]

Integrable conditional expectation is linear and satisfies the modulus bound. (Basic algebra and order properties of conditional expectation)

[F3]

A common integrable dominator and almost-sure convergence give integrability and $L^{1}$ convergence. (Dominated convergence)

[F4]

Under AC integrable conditional classes and their versions exist. (Conditional expectation as an ae class)

[F5]

Countable infima and liminf of measurable functions are measurable. (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable)

Proof

technique · direct

1.1

Put $Z_{n} = \inf_{k \geq n} X_{k}$ . These are measurable by [F5], nonnegative, and increase to ${lim inf}_{k} X_{k}$ . For each $k \geq n$ , [F1] gives $E [Z_{n} ∣ G] \leq E [X_{k} ∣ G]$ almost surely. There are only countably many pairs $(n, k)$ ; after removing their null union, take the infimum over $k \geq n$ and then the increasing limit in $n$ . Conditional MCT gives exactly the claimed Fatou inequality.

F1F5

2.1

In the dominated case, $∣ X ∣ \leq W$ almost surely, so [F3] gives $X \in L^{1}$ . Set $T = E [W ∣ G]$ , $U_{n} = E [X_{n} ∣ G]$ and $U = E [X ∣ G]$ . These are finite almost surely. Apply step 1.1 to $W + X_{n}$ and $W - X_{n}$ , which are nonnegative. By linearity this gives $T + U \leq T + lim inf U_{n}$ and $T - U \leq T - lim sup U_{n}$ . The modulus bound gives $∣ U_{n} ∣, ∣ U ∣ \leq T$ outside one common null set. Subtracting the finite $T$ yields $U \leq lim inf U_{n} \leq lim sup U_{n} \leq U$ , hence almost-sure convergence.

step 1.1F2F3F4

3.1

The differences $∣ U_{n} - U ∣$ tend to zero almost surely and are bounded by $2 T$ , with $E T = E W < \infty$ . Ordinary DCT therefore gives $E ∣ U_{n} - U ∣ \to 0$ , the claimed $L^{1}$ convergence.

step 2.1F2F3∎

Source notes

Van der Vaart Lemma 1.10(ii)–(iii), printed p.4, full statements read; ordinary MCT, conditional order and the two nonnegative dominated sequences supply the proof here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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, 5th ed. (standard reference, not scraped)