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.
Rational conditional distribution functions produce real regular kernels
Statement
Assume AC. Let be a real random variable on , and . Rational versions and as in Simultaneous rational conditional distribution function versions determine a probability kernel with
For every Borel and ,
Thus is a regular conditional distribution of , everywhere a probability measure.
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
There are rational conditional versions with simultaneous bounds, monotonicity, tails and rational right limits; the same lemma locally establishes monotone convergence and bounded decreasing convergence from the repaired simple-integral foundation. Simultaneous rational conditional distribution function versions.
Under countable choice, a nondecreasing right-continuous function with tails zero and one has a Borel probability with the prescribed closed-half-line values. Only this existence clause is used; uniqueness is proved locally below. Probability laws correspond to distribution functions.
A lambda-system containing a pi-system contains its generated sigma-algebra. Dynkin's pi-lambda theorem.
Rational right rays, and therefore their closed-left-ray complements, generate the Borel sets. Seven generating families for the Borel sigma-algebra on the real line.
Countable infima and pointwise limits are measurable. Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable.
AC supplies the preceding version selection and countable choice for CDF existence; unique specification needs no further choice. The Axiom of Choice.
Between any two distinct reals lies a rational. The rationals embed densely in the reals.
The rationals admit a fixed enumeration. is countably infinite.
Proof
Use the everywhere good filled data of [F1], writing them again . For fixed , put . The index set is nonempty by F7 and countable by F8. Its values lie in , and shrinking it as increases shows monotonicity. For rational , monotonicity of the data gives for every positive integer , so the rational right-limit condition gives . In particular and , and monotonicity gives both real tail limits.
If , monotonicity gives a limit . For every rational , eventually , so and . Taking the infimum gives . In particular the sequence proves right continuity. By the existence clause of [F2] there is a Borel probability with CDF . If are two such probabilities, the equality class contains and every closed half-line, is closed under complements by subtraction from the common finite total one, and is closed under countable disjoint unions by countable additivity. It is a lambda-system containing the closed-half-line pi-system, whose generated sigma-algebra is Borel by [F4]; [F3] gives . Thus the probability is locally proved unique and defines without a family choice. On its CDF is , so the same uniqueness identifies it with .
For fixed real , [F5] makes a -measurable countable infimum. Using F7 and the fixed enumeration in F8, choose recursively the first enumerated rational and then the first ; thus . Step 2.1 and rational agreement give . The bounded decreasing-convergence clause locally proved in [F1], applied on , gives The last indicator limit includes the point .
Let be the Borel sets for which is -measurable and the stated identity holds for every . It contains . Complements use and subtraction from the finite total . For pairwise disjoint , countable additivity of each section gives the union evaluation as the increasing limit of finite partial sums. This is measurable by [F5], and the locally proved monotone convergence in [F1] gives the event identity. Hence is a lambda-system containing the closed-half-line pi-system from step 3.1. By [F3] and [F4] it contains every Borel set. The measurable evaluations and probability sections prove both kernel axioms and the full conditional identity.
Depends on
- Simultaneous rational conditional distribution function versions
- Probability laws correspond to distribution functions
- Dynkin's pi-lambda theorem
- Seven generating families for the Borel sigma-algebra on the real line
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
- The rationals embed densely in the reals
- $\mathbb{Q}$ is countably infinite
- The Axiom of Choice
Used by
Dependency tree · two levels
58 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, fifth edition (standard reference, not scraped)
- Varadhan, Probability Theory, Chapter 4 (standard reference, not scraped)