Independence From a Trivial Sigma-Algebra

This is an independence lemma for a null-or-conull sub-$\sigma$-algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space, and let $m,m'$ be measurable spaces on $\Omega$ with $m\subseteq\mathcal F$. Assume IsTrivialSigma P m, meaning that every $m$-measurable set has $P$-measure either $0$ or $1$. Then $m$ and $m'$ are independent under $P$:

The conclusion is independent of any further relation between $m'$ and the ambient measurable space. This is a reusable technical result for discarding null-or-conull factors from independence arguments.

Original Lean declaration header

Within namespace LevyStochCalc.Probability. Shown in its original module context. Proof omitted.

theorem IsTrivialSigma.indep [IsProbabilityMeasure P] {m m' : MeasurableSpace Ω}
    (hm : m ≤ mΩ) (h : IsTrivialSigma P m) : Indep m m' P

Module navigation

Module: LevyStochCalc/Probability/TrivialSigma.

Next: isTrivialSigma_comap_of_ae_const.

Source excerpt, lines 36–37 · Frozen source 408915f.