Regular conditional distributions

StructureRegular conditional distribution (measure-valued family)#✓fully proved

Let \(P\) be a measure on a measurable space \((\Omega, \mathcal{F})\), let \(S\) be a measurable space, \(X : \Omega \to S\) a map, \(\mathcal{G}\) a σ-algebra on \(\Omega\), and \(\rho\) a family assigning a measure \(\rho_\omega\) on \(S\) to each \(\omega \in \Omega\). Then \(\rho\) is a regular conditional distribution of \(X\) given \(\mathcal{G}\) under \(P\) if \(\mathcal{G} \subseteq \mathcal{F}\); \(X\) is \(\mathcal{F}\)-measurable; for every measurable \(A \subseteq S\) the map \(\omega \mapsto \rho_\omega(A)\) is \(\mathcal{G}\)-measurable; \(\rho_\omega(S) \le 1\) for every \(\omega\); for every measurable \(A \subseteq S\) the real number \(\rho_\omega(A)\) agrees, for \(P\)-almost every \(\omega\), with the conditional expectation \(P[\mathbf{1}_{X^{-1}(A)} \mid \mathcal{G}](\omega)\); and \(\rho_\omega\) is a probability measure for \(P\)-almost every \(\omega\).

Because each \(\rho_\omega\) is a measure, countable additivity holds at every sample point, including null ones; this is stricter than the raw set-function definition of Lecture 26, whose set functions need to form probability measures only almost everywhere.

structure RegularConditionalDistribution
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Type*} [MeasurableSpace S]
    (rcd : Ω → Measure S) (X : Ω → S) (𝒢 : MeasurableSpace Ω)
    (P : @Measure Ω mΩ) : Prop where
  conditioning_le : 𝒢 ≤ mΩ
  measurable_target : @Measurable Ω S mΩ ‹MeasurableSpace S› X
  measurable_eval : ∀ {A : Set S}, MeasurableSet A →
    Measurable[𝒢] fun ω => rcd ω A
  mass_le_one : ∀ ω, rcd ω Set.univ ≤ 1
  ae_eq_condexp : ∀ {A : Set S}, MeasurableSet A →
    (fun ω => (rcd ω A).toReal) =ᵐ[P] P⟦X ⁻¹' A | 𝒢⟧
  ae_isProbabilityMeasure : ∀ᵐ ω ∂P, IsProbabilityMeasure (rcd ω)

Used by 2

Used byExistence of measure-valued regular conditional distributions given a sub-σ-algebra · Existence of measure-valued regular conditional distributions given a random variable

StructureRegular conditional distribution (kernel form)#✓fully proved

Let \(\mu\) be a measure on \(\alpha\) and let \(X : \alpha \to \beta\) and \(Y : \alpha \to \Omega\) be maps. A kernel \(\kappa\) from \(\beta\) to \(\Omega\) is a regular conditional distribution of \(Y\) given \(X\) under \(\mu\) if \(X\) and \(Y\) are measurable, \(\kappa\) is a Markov kernel, and for every measurable set \(s \subseteq \Omega\) the real-valued function \(a \mapsto \kappa(X(a))(s)\) is \(\mu\)-almost everywhere equal to the conditional expectation \(\mu[\mathbf{1}_{Y^{-1}(s)} \mid \sigma(X)]\), where \(\sigma(X)\) is the σ-algebra on \(\alpha\) generated by \(X\).

structure IsRegularConditionalDistribution
    (κ : Kernel β Ω) (Y : α → Ω) (X : α → β) (μ : Measure α) : Prop where
  measurable_conditioning : @Measurable α β mα mβ X
  measurable_target : @Measurable α Ω mα ‹MeasurableSpace Ω› Y
  isMarkovKernel : IsMarkovKernel κ
  ae_eq_condExp : ∀ {s : Set Ω}, MeasurableSet s →
    (fun a => (κ (X a)).real s) =ᵐ[μ] μ⟦Y ⁻¹' s | mβ.comap X⟧

Used by 2

Used byThe conditional distribution kernel is a regular conditional distribution · Existence of regular conditional distributions (kernel form)

TheoremThe conditional distribution kernel is a regular conditional distribution#✓fully proved

Let \(\Omega\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(\alpha\), and \(X : \alpha \to \beta\), \(Y : \alpha \to \Omega\) measurable maps. Then the conditional distribution of \(Y\) given \(X\) under \(\mu\), the kernel from \(\beta\) to \(\Omega\) obtained by disintegrating the joint law of \((X, Y)\) under \(\mu\), is a regular conditional distribution of \(Y\) given \(X\) under \(\mu\).

theorem condDistrib_isRegularConditionalDistribution
    [StandardBorelSpace Ω] [Nonempty Ω] [IsFiniteMeasure μ]
    {X : α → β} {Y : α → Ω}
    (hX : Measurable X) (hY : Measurable Y) :
    IsRegularConditionalDistribution (condDistrib Y X μ) Y X μ

Uses 1 · Used by 1

Statement usesRegular conditional distribution (kernel form)

Used byExistence of regular conditional distributions (kernel form)

TheoremExistence of regular conditional distributions (kernel form)#✓fully proved

Let \(\Omega\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(\alpha\), and \(X : \alpha \to \beta\), \(Y : \alpha \to \Omega\) measurable maps. Then there exists a kernel \(\kappa\) from \(\beta\) to \(\Omega\) that is a regular conditional distribution of \(Y\) given \(X\) under \(\mu\); in particular \(\kappa\) is a Markov kernel.

theorem exists_regularConditionalDistribution
    [StandardBorelSpace Ω] [Nonempty Ω] [IsFiniteMeasure μ]
    {X : α → β} {Y : α → Ω}
    (hX : Measurable X) (hY : Measurable Y) :
    ∃ κ : Kernel β Ω, IsRegularConditionalDistribution κ Y X μ

Uses 2

Statement usesRegular conditional distribution (kernel form)

Proof usesThe conditional distribution kernel is a regular conditional distribution

TheoremExistence of measure-valued regular conditional distributions given a sub-σ-algebra#✓fully proved

Let \(\Omega\) be a nonempty standard Borel space, \(\mu\) a finite measure on a measurable space \((\alpha, \mathcal{F})\), \(\mathcal{G} \subseteq \mathcal{F}\) a sub-σ-algebra, and \(Y : \alpha \to \Omega\) an \(\mathcal{F}\)-measurable map. Then some family of measures on \(\Omega\) indexed by \(\alpha\) is a measure-valued regular conditional distribution of \(Y\) given \(\mathcal{G}\) under \(\mu\).

The witness is the conditional distribution of \(Y\) given the identity map from \((\alpha, \mathcal{F})\) to \((\alpha, \mathcal{G})\).

theorem exists_regularConditionalDistribution_family_of_le
    [StandardBorelSpace Ω] [Nonempty Ω] [IsFiniteMeasure μ]
    {𝒢 : MeasurableSpace α} {Y : α → Ω}
    (h𝒢 : 𝒢 ≤ mα) (hY : @Measurable α Ω mα ‹MeasurableSpace Ω› Y) :
    ∃ rcd : α → Measure Ω, RegularConditionalDistribution rcd Y 𝒢 μ

Uses 1 · Used by 1

Statement usesRegular conditional distribution (measure-valued family)

Used byExistence of measure-valued regular conditional distributions given a random variable

TheoremExistence of measure-valued regular conditional distributions given a random variable#✓fully proved

Let \(\Omega\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(\alpha\), and \(X : \alpha \to \beta\), \(Y : \alpha \to \Omega\) measurable maps. Then some family of measures on \(\Omega\) indexed by \(\alpha\) is a measure-valued regular conditional distribution of \(Y\) given the σ-algebra \(\sigma(X)\) on \(\alpha\) generated by \(X\), under \(\mu\).

theorem exists_regularConditionalDistribution_family
    [StandardBorelSpace Ω] [Nonempty Ω] [IsFiniteMeasure μ]
    {X : α → β} {Y : α → Ω}
    (hX : Measurable X) (hY : Measurable Y) :
    ∃ rcd : α → Measure Ω,
      RegularConditionalDistribution rcd Y (mβ.comap X) μ

Uses 2

Statement usesRegular conditional distribution (measure-valued family)

Proof usesExistence of measure-valued regular conditional distributions given a sub-σ-algebra

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.