Conditional Independence - Basic Definitions and Properties

This file defines conditional independence for random variables and establishes basic properties. The definition uses indicator functions on measurable rectangles.

Main definitions

• CondIndep Y Z W μ: Y and Z are conditionally independent given W under measure μ, denoted Y ⊥⊥_W Z, defined via indicator test functions on Borel sets.

Main results

• condIndep_symm: Conditional independence is symmetric (Y ⊥⊥_W Z ↔ Z ⊥⊥_W Y)

Implementation notes

We use an indicator-based characterization rather than σ-algebra formalism to avoid requiring a full conditional distribution API. The definition states that for all Borel sets A, B:

E[1_A(Y) · 1_B(Z) | σ(W)] = E[1_A(Y) | σ(W)] · E[1_B(Z) | σ(W)] a.e.

This is equivalent to the standard σ-algebra definition but more elementary to work with.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Section 6.1
• Kallenberg (2002), Foundations of Modern Probability, Chapter 6

Definition of conditional independence

def CondIndep {Ω : Type u_5} {α : Type u_6} {β : Type u_7} {γ : Type u_8} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) : Prop

Conditional independence via indicator test functions.

Random variables Y and Z are conditionally independent given W under measure μ, denoted Y ⊥⊥_W Z, if for all Borel sets A and B:

E[1_A(Y) · 1_B(Z) | σ(W)] = E[1_A(Y) | σ(W)] · E[1_B(Z) | σ(W)] a.e.

Mathematical content: This says that knowing W, the events {Y ∈ A} and {Z ∈ B} are independent: P(Y ∈ A, Z ∈ B | W) = P(Y ∈ A | W) · P(Z ∈ B | W).

Why indicators suffice: By linearity and approximation, this extends to all bounded measurable functions. The key is that indicators generate the bounded measurable functions via monotone class arguments.

Relation to σ-algebra definition: This is equivalent to σ(Y) ⊥⊥_σ(W) σ(Z), but stated more elementarily without requiring full conditional probability machinery.

Implementation: We use Set.indicator for the characteristic function 1_A.

Equations

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

Basic properties

theorem condIndep_symm {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) : CondIndep μ Y Z W ↔ CondIndep μ Z Y W

Symmetry of conditional independence.

If Y ⊥⊥_W Z, then Z ⊥⊥_W Y. This follows immediately from commutativity of multiplication.