Directing Kernel for de Finetti's Theorem

This file defines the directing kernel ν for de Finetti's theorem. The kernel gives the conditional distribution of the first coordinate given the shift-invariant σ-algebra.

Main definitions

• π0: Projection onto the first coordinate
• rcdKernel: Regular conditional distribution kernel
• ν: The directing measure as a function Ω[α] → Measure α

Main results

• integral_ν_eq_integral_condExpKernel: Key bridge lemma relating integrals against ν to integrals against the conditional expectation kernel

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1

Coordinate projection

def Exchangeability.DeFinetti.ViaKoopman.π0 {α : Type u_1} : Ω[α] → α

Projection onto the first coordinate.

Equations

• Exchangeability.DeFinetti.ViaKoopman.π0 ω = ω 0

theorem Exchangeability.DeFinetti.ViaKoopman.measurable_pi0 {α : Type u_1} [MeasurableSpace α] : Measurable π0

Regular conditional distribution kernel

noncomputable def Exchangeability.DeFinetti.ViaKoopman.rcdKernel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] : ProbabilityTheory.Kernel Ω[α] α

Regular conditional distribution kernel constructed via condExpKernel.

This is the kernel giving the conditional distribution of the first coordinate given the tail σ-algebra.

Equations

• One or more equations did not get rendered due to their size.

instance Exchangeability.DeFinetti.ViaKoopman.rcdKernel_isMarkovKernel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] : ProbabilityTheory.IsMarkovKernel rcdKernel

noncomputable def Exchangeability.DeFinetti.ViaKoopman.ν {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] : Ω[α] → MeasureTheory.Measure α

The regular conditional distribution as a function assigning to each point a probability measure on α.

Equations

• Exchangeability.DeFinetti.ViaKoopman.ν ω = Exchangeability.DeFinetti.ViaKoopman.rcdKernel ω

theorem Exchangeability.DeFinetti.ViaKoopman.ν_eval_measurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] {s : Set α} (hs : MeasurableSet s) : Measurable fun (ω : Ω[α]) => (ν ω) s

ν evaluation on measurable sets is measurable in the parameter.

instance Exchangeability.DeFinetti.ViaKoopman.ν_isProbabilityMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (ω : Ω[α]) : MeasureTheory.IsProbabilityMeasure (ν ω)

ν ω is a probability measure for each ω.

Bridge lemmas

theorem Exchangeability.DeFinetti.ViaKoopman.integral_ν_eq_integral_condExpKernel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (ω : Ω[α]) {f : α → ℝ} (hf : Measurable f) : ∫ (x : α), f x ∂ν ω = ∫ (y : Ω[α]), f (y 0) ∂(ProbabilityTheory.condExpKernel μ shiftInvariantSigma) ω

Helper: Integral against ν relates to integral against condExpKernel via coordinate projection.

This lemma makes explicit how integrating a function f : α → ℝ against the conditional distribution ν ω relates to integrating f ∘ π₀ against condExpKernel μ m ω.