Conditional Independence - Bounded Measurable Extension

This file re-exports the bounded measurable extension infrastructure for conditional independence.

Module structure

• Bounded/Projection.lean - Projection theorems for conditional expectations

Main results (re-exported)

• condExp_project_of_condIndep: Conditional expectation projection theorem

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Section 6.1