Directing Measure Core: CDF and Measure Construction #
This file defines the core components of the directing measure construction:
cdf_from_alpha: The regularized CDF built from alpha functions via Stieltjes extensiondirecting_measure: The probability measure on ℝ for each ω ∈ Ωdirecting_measure_isProbabilityMeasure: Proof that ν(ω) is a probability measure
Main definitions #
cdf_from_alpha: CDF function F(ω,t) viastieltjesOfMeasurableRatdirecting_measure: The directing measure ν : Ω → Measure ℝ
Main results #
cdf_from_alpha_mono: F(ω,·) is monotone nondecreasingcdf_from_alpha_rightContinuous: F(ω,·) is right-continuouscdf_from_alpha_bounds: 0 ≤ F(ω,t) ≤ 1alphaIic_ae_tendsto_zero_at_bot: a.e. limit 0 at -∞ for alphaIicalphaIic_ae_tendsto_one_at_top: a.e. limit 1 at +∞ for alphaIicdirecting_measure_isProbabilityMeasure: ν(ω) is a probability measure for each ω
References #
- Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"
CDF Construction #
The CDF F(ω,t) is built from the rational-valued alpha functions using
mathlib's stieltjesOfMeasurableRat construction, which automatically:
- Patches the null set where CDF properties might fail
- Ensures right-continuity and proper limits
- Produces a valid probability measure via Carathéodory extension
CDF function constructed from the alpha conditional expectations. This is the right-continuous version obtained via Stieltjes extension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F(ω,·) is monotone nondecreasing.
Right-continuity in t: F(ω,t) = lim_{u↘t} F(ω,u).
Bounds 0 ≤ F ≤ 1 (pointwise in ω,t).
A.e. endpoint limits for alphaIic #
These lemmas establish a.e. convergence of alphaIic at ±∞ by combining:
- The a.e. equality
alphaIic =ᵐ alphaIicCE(from AlphaConvergence) - The a.e. convergence of
alphaIicCE(from AlphaConvergence)
A.e. convergence of α_{Iic t} → 0 as t → -∞ (along integers).
This is the a.e. version of the endpoint limit. The statement for all ω cannot be
proven from the L¹ construction since alphaIic is defined via existential L¹ choice.
Proof strategy:
Combine the a.e. equality alphaIic =ᵐ alphaIicCE with alphaIicCE_ae_tendsto_zero_atBot.
Since both are a.e. statements and we take countable intersection over integers, we
get a.e. convergence of alphaIic along the integer sequence -(n:ℝ).
A.e. convergence of α_{Iic t} → 1 as t → +∞ (along integers).
This is the dual of alphaIic_ae_tendsto_zero_at_bot. The statement for all ω cannot be
proven from the L¹ construction since alphaIic is defined via existential L¹ choice.
Proof strategy:
Combine the a.e. equality alphaIic =ᵐ alphaIicCE with alphaIicCE_ae_tendsto_one_atTop.
Directing Measure Definition #
The directing measure ν(ω) is built from the CDF via mathlib's
stieltjesOfMeasurableRat.measure construction. This automatically
handles the null set patching and produces a probability measure for ALL ω.
Build the directing measure ν from the CDF.
For each ω ∈ Ω, we construct ν(ω) as the probability measure on ℝ with CDF given by t ↦ cdf_from_alpha X ω t.
This is defined directly using stieltjesOfMeasurableRat.measure, which gives a
probability measure for ALL ω (not just a.e.) because the stieltjesOfMeasurableRat
construction patches the null set automatically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The directing measure is a probability measure.
This is now trivial because directing_measure is defined via stieltjesOfMeasurableRat.measure,
which automatically has an IsProbabilityMeasure instance from mathlib.