Alphabeta Math
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 Xn, E[lim inf⁡nXn∣G]≤lim inf⁡nE[Xn∣G] almost surely, in the extended sense. If real-valued measurable Xn and X satisfy Xn→X almost surely and ∣Xn∣≤W almost surely for one nonnegative W∈L1(P), then E[Xn∣G]→E[X∣G] almost surely and in L1.

Facts & Assumptions

Given: AC and nonnegative measurable Xn; separately real-valued measurable Xn and X such that Xn→X almost surely and ∣Xn∣≤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 L1 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.1F1F5

Put Zn=inf⁡k≥nXk. These are measurable by [F5], nonnegative, and increase to lim inf⁡kXk. For each k≥n, [F1] gives E[Zn∣G]≤E[Xk∣G] almost surely. There are only countably many pairs (n,k); after removing their null union, take the infimum over k≥n and then the increasing limit in n. Conditional MCT gives exactly the claimed Fatou inequality.

2.1step 1.1F2F3F4

In the dominated case, ∣X∣≤W almost surely, so [F3] gives X∈L1. Set T=E[W∣G], Un=E[Xn∣G] and U=E[X∣G]. These are finite almost surely. Apply step 1.1 to W+Xn and W−Xn, which are nonnegative. By linearity this gives T+U≤T+lim inf⁡Un and T−U≤T−lim sup⁡Un. The modulus bound gives ∣Un∣,∣U∣≤T outside one common null set. Subtracting the finite T yields U≤lim inf⁡Un≤lim sup⁡Un≤U, hence almost-sure convergence.

3.1step 2.1F2F3∎

The differences ∣Un−U∣ tend to zero almost surely and are bounded by 2T, with ET=EW<∞. Ordinary DCT therefore gives E∣Un−U∣→0, the claimed L1 convergence.

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

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