Alphabeta Math
LemmaStatement: 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.

Simultaneous rational conditional distribution function versions

Statement

Assume AC. Let X:ΩR be measurable on a probability space (Ω,F,P) and GF a sub-sigma-algebra. There are real G-measurable versions Gq of P(XqG) for every qQ and one NG, P(N)=0, such that outside N, simultaneously,

0Gq1,q<rGqGr,Gn1,Gn0,Gq+1/nGq.

Here n=1,2, and the final assertion holds for every rational q. The versions may moreover be filled on N by Gq=1{q0}, so all these properties hold everywhere.

The proof also establishes the restricted integral interface used here and below: arbitrary nonnegative simple displays give the same integral after zero-complement refinement; the resulting nonnegative integral is monotone, additive, positively homogeneous, has 0=0 as a separate zero-scalar clause, and satisfies monotone convergence. On a finite measure space, bounded decreasing convergence follows. Under AC, every event has a bounded conditional-density version, unique almost surely, and these versions preserve inclusion, constants, and monotone event limits.

Facts & Assumptions

Given: The hypotheses and conventions in the statement.

[F1]

The simple and nonnegative integrals are respectively the finite coefficient sum with 0(+)=0 and the supremum over nonnegative simple minorants. The integral of a nonnegative simple function, The nonnegative Lebesgue integral, Integral over a measurable subset.

[F2]

Every nonnegative measurable function has prescribed increasing simple approximants. Every nonnegative measurable function is the increasing limit of simple measurable functions.

[F3]

Hahn decomposition applies to the finite signed measures used in the density construction. Hahn decomposition for signed measures, unique up to total-variation-null sets.

[F4]

Measures are countably additive and continuous from below. Measures on sigma-algebras, Continuity from below for measures.

[F5]

AC selects maximizing sequences, Hahn decompositions and the rational family of densities. The Axiom of Choice.

[F6]

The rationals and their finite products are countable. Q is countably infinite, A product of two at most countable sets is at most countable.

[F7]

A specified countable union of measurable null sets is null. Finite and countable subadditivity of measures.

[F8]

Limsup, liminf and convergence sets of measurable functions are measurable. Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable.

Proof

technique · direct
1.1

We first repair the integral interface. Given two finite disjoint simple displays s=ici1Ei=jdj1Fj, adjoin E0=ΩiEi and F0=ΩjFj, both with coefficient zero. The intersections EiFj, now including indices zero, form a finite measurable partition of all of Ω. On every nonempty cell the two coefficients agree, so finite additivity gives equal coefficient sums. This includes infinite-measure zero cells because both corresponding products are the stipulated 0(+)=0. Thus the simple integral in [F1] is representation-independent. A common zero-complement refinement now proves monotonicity and additivity for simple functions. For a scalar a>0, termwise multiplication proves positive homogeneity; for a=0, the zero display gives 0=0 directly, without forming 0(+).

F1F4construct
2.1

The supremum definition in [F1] therefore gives monotonicity of the nonnegative integral and agreement with the simple integral. Multiplication by a>0 bijects the simple minorants of f and af, giving positive homogeneity; again 0=0 is separate. If 0fnf, let L=supnfn. For a simple sf and 0<a<1, put An={fnas}. Then AnΩ. The formula AAs is a measure by the finite partition formula from step 1.1, so [F4] gives Anss. Since as1Anfn, positive homogeneity gives aAnsL; let first n and then a1 to obtain sL. Taking the supremum over s proves monotone convergence. Using the approximants in [F2], simple additivity and monotone convergence give (f+g)=f+g. Consequently AAf is a measure: apply monotone convergence to finite unions of a disjoint sequence. If the ambient measure is finite and 0fnfM, then MfnMf; additivity in the finite identity fn+(Mfn)=M proves bounded decreasing convergence.

step 1.1F1F2F4
3.1

We next construct conditional densities without importing a conditional-expectation theorem. For an event CF, set νC(A)=P(AC) on G. Let H be the nonnegative measurable h satisfying AhdPνC(A) for every AG, and let M=suphHhdP1. The maximum of two members remains in H: split each test event over {hk} and its complement and use step 2.1. By [F5] choose hjH with integrals tending to M, and put fj=maxijhif. By F8 the supremum f is measurable. Step 2.1 gives fH and f=M. The set function ρ(A)=νC(A)AfdP is a finite positive measure. If it were not singular to PG, choose by [F3] a positive set Qm for ρP/m for every m1. If every P(Qm)=0, their union is null by [F7], and on its complement ρ(A)P(A)/m for every m, so ρ is concentrated on a P-null set, a contradiction. Hence some Qm has positive P-measure, and f+m11QmH has integral greater than M, again a contradiction. Thus ρP. Since 0ρνCP, it is also absolutely continuous, so its singular carrier immediately gives ρ=0. We have proved νC(A)=AfdP for all AG.

step 2.1F3F5F7F8assume-contracontradiction: maximalitydischarge-contradiction
4.1

Since f1, the sets {fn} show that f< almost surely. Comparing νCP on {f1+1/m} shows that f1 almost surely. Changing f on the measurable union of these null sets gives a real [0,1]-valued density. If f,g represent νC,νD and CD, then on Am={fg+1/m}, step 2.1 gives AmfAmg+P(Am)/m, whereas the representation identities give AmfAmg. Hence P(Am)=0 for every m, so fg almost surely. Taking C=D in both directions proves uniqueness; C=,Ω proves the constant-zero and constant-one assertions. For CjC, set all selected densities to zero on the countable union of their order failures and put u=limjfj. Step 2.1 and [F4] give Au=limjP(ACj)=P(AC), so uniqueness identifies u with the density of C. Decreasing event limits follow by applying this to complements and using A(1f)=P(A)Af, an instance of the finite additivity from step 2.1. This proves every restricted conditional-density assertion in the statement.

step 2.1step 3.1F4F7
5.1

Apply step 3.1 to Cq={Xq} and use [F5] to select one real G-measurable density Gq for each rational q. The selection is countable by [F6]. Step 4.1 gives 0Gq1 almost surely and GqGr almost surely whenever q<r. Since CnΩ, Cn, and Cq+1/nCq, the event-limit clause of step 4.1 gives the two tail limits and every rational right-limit almost surely.

step 3.1step 4.1F5F6
6.1

Form the union N of the failure sets for the bounds, rational order comparisons, two tail limits, and the right-limit assertion for each rational q. They belong to G by rational-cut descriptions and [F8], and they are null by step 5.1. There are countably many by [F6], so [F7] gives P(N)=0. Replace each Gq on N by 1{q0}. Pasting preserves measurability. A bounded difference supported on N has absolute value at most a constant times 1N, whose integral is zero by step 2.1, so all event integrals are unchanged and the functions remain versions. The filler is increasing, has the required tails, and satisfies the right-limit property also at q=0.

step 2.1step 5.1F6F7F8

Depends on

Used by

Dependency tree · two levels

47 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