Canonical Conditional Expectation Version of Alpha_Iic #
This file defines alphaIicCE, the canonical conditional expectation version of
the CDF-building function alphaIic. This is the "best" representative of the
L¹ equivalence class, with good a.e. properties.
Main definitions #
alphaIicCE: Conditional expectationE[1_{(-∞,t]}(X₀) | tail σ-algebra]
Main results #
alphaIicCE_measurable:alphaIicCEis measurablealphaIicCE_mono:alphaIicCEis monotone in t (a.e.)alphaIicCE_nonneg_le_one:0 ≤ alphaIicCE ≤ 1(a.e.)alphaIicCE_right_continuous_at: Right-continuity at any real t (a.e.)alphaIicCE_iInf_rat_gt_eq: Right-continuity at rationals (a.e.)
References #
- Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"
Canonical conditional expectation version of alphaIic #
The existential α from weighted_sums_converge_L1 is unique in L¹ up to a.e. equality.
We now define the canonical version using conditional expectation onto the tail σ-algebra.
This avoids all pointwise headaches and gives us the endpoint limits for free.
Canonical conditional expectation version of α_{Iic t}.
This is the conditional expectation of the indicator function 1_{(-∞,t]}∘X_0 with respect
to the tail σ-algebra. By the reverse martingale convergence theorem, this equals the
existential alphaIic almost everywhere.
Key advantages:
- Has pointwise bounds
0 ≤ alphaIicCE ≤ 1everywhere (not just a.e.) - Monotone in
talmost everywhere (from positivity of conditional expectation) - Endpoint limits follow from L¹ contraction and dominated convergence
Equations
- Exchangeability.DeFinetti.ViaL2.alphaIicCE X hX_contract hX_meas hX_L2 t = μ[Exchangeability.DeFinetti.ViaL2.indIic t ∘ X 0|Exchangeability.DeFinetti.ViaL2.TailSigma.tailSigma X]
Instances For
Measurability of alphaIicCE.
Note: Previously had BorelSpace typeclass instance resolution issues.
The conditional expectation condExp μ (tailSigma X) f is measurable by
stronglyMeasurable_condExp.measurable, but Lean can't synthesize the required
BorelSpace instance automatically. This should be straightforward to fix.
alphaIicCE is monotone nondecreasing in t (for each fixed ω).
alphaIicCE is bounded in [0,1] almost everywhere.
Right-continuity of alphaIicCE at any real t.
For any real t, the infimum over rationals greater than t is at most the value at t:
⨅ q > t (rational), alphaIicCE q ω ≤ alphaIicCE t ω a.e.
Combined with monotonicity (which gives the reverse inequality), this proves the infimum equals the value.
Proof strategy:
- Indicators 1_{Iic s} are right-continuous in s: as s ↓ t, 1_{Iic s} ↓ 1_{Iic t}
- By dominated convergence for condExp, E[1_{Iic s}(X₀)|tail] → E[1_{Iic t}(X₀)|tail] in L¹
- For monotone decreasing sequences, L¹ convergence + boundedness ⇒ a.e. convergence
- Therefore ⨅ s > t, alphaIicCE s = alphaIicCE t a.e.
Note: Uses dominated convergence for conditional expectations. The mathematical argument is standard: for CDFs built from conditional expectations, right-continuity follows from dominated convergence applied to decreasing indicators.
Right-continuity of alphaIicCE at rationals.
For each rational q, the infimum from the right equals the value:
⨅ r > q (rational), alphaIicCE r = alphaIicCE q a.e.
Proof strategy:
- alphaIicCE is monotone (increasing in t)
- For rₙ ↓ q, the indicators 1_{Iic rₙ} ↓ 1_{Iic q} pointwise
- By dominated convergence: E[1_{Iic rₙ}(X₀)|tail] → E[1_{Iic q}(X₀)|tail] in L¹
- For monotone sequences, L¹ convergence implies a.e. convergence
- So alphaIicCE rₙ → alphaIicCE q a.e. for any sequence rₙ ↓ q
- This means ⨅ r > q, alphaIicCE r = alphaIicCE q a.e.