Helper Lemmas for RN-Derivative Approach to Kallenberg 1.3 #
This file provides helper lemmas for the Radon-Nikodym derivative approach to Kallenberg Lemma 1.3 (contraction-independence).
Main results #
marginal_law_eq_of_pair_law: From(X,W) =^d (X,W'), extractW =^d W'joint_measure_eq_of_pair_law: Restricted measure equality from pair lawintegral_sq_condExp_eq_of_pair_law: Square integrals equal via Doob-Dynkin
References #
- Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Lemma 1.3
theorem
marginal_law_eq_of_pair_law
{Ω : Type u_1}
{α : Type u_2}
{γ : Type u_3}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
(X : Ω → α)
(W W' : Ω → γ)
(hX : Measurable X)
(hW : Measurable W)
(hW' : Measurable W')
(h_law :
MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W' ω)) μ)
:
From pair law equality (X,W) =^d (X,W'), extract marginal law equality W =^d W'.
theorem
joint_measure_eq_of_pair_law
{Ω : Type u_1}
{α : Type u_2}
{γ : Type u_3}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
(X : Ω → α)
(W W' : Ω → γ)
(hX : Measurable X)
(hW : Measurable W)
(hW' : Measurable W')
(h_law :
MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W' ω)) μ)
{A : Set α}
(hA : MeasurableSet A)
:
MeasureTheory.Measure.map W (μ.restrict (X ⁻¹' A)) = MeasureTheory.Measure.map W' (μ.restrict (X ⁻¹' A))
From pair law equality, derive joint measure equality on the conditioning space.
If (X,W) =^d (X,W'), then map W (μ.restrict (X ⁻¹' A)) = map W' (μ.restrict (X ⁻¹' A)).
Intuitively: "the law of W restricted to {X ∈ A}" equals "the law of W' restricted to {X ∈ A}".
theorem
integral_sq_condExp_eq_of_pair_law
{Ω : Type u_1}
{α : Type u_2}
{γ : Type u_3}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(X : Ω → α)
(W W' : Ω → γ)
(hX : Measurable X)
(hW : Measurable W)
(hW' : Measurable W')
(h_law :
MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W' ω)) μ)
{A : Set α}
(hA : MeasurableSet A)
:
∫ (ω : Ω), μ[(X ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance] ω * μ[(X ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance] ω ∂μ = ∫ (ω : Ω), μ[(X ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W' inferInstance] ω * μ[(X ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W' inferInstance] ω ∂μ
Helper for Kallenberg 1.3: Square integrals are equal via Doob-Dynkin factorization.
Given:
(X,W) =^d (X,W')(pair laws equal, hence ρ = law(W) = law(W'))μ₁ = E[φ|σ(W)]andμ₂ = E[φ|σ(W')]where φ = 1_{X∈A}
This lemma proves ∫ μ₁² dμ = ∫ μ₂² dμ using:
- Doob-Dynkin: μ₁ = g₁ ∘ W, μ₂ = g₂ ∘ W' for measurable g₁, g₂
- Set-integral uniqueness: g₁ = g₂ ρ-a.e.
- Change of variables: ∫ μ₁² dμ = ∫ g₁² dρ = ∫ g₂² dρ = ∫ μ₂² dμ