Triviality of the Sigma-Algebra of an Almost-Surely Constant Map

This establishes triviality for a sigma-algebra generated by an almost-surely constant random variable.

Let $(\Omega,\mathcal F,P)$ be a probability space, let $\mathcal Y$ be a measurable space, let $f:\Omega\to\mathcal Y$, and let $y\in\mathcal Y$. Assume

$f(\omega)=y\quad\text{for $P$-almost every }\omega.$

Then the comap sigma-algebra MeasurableSpace.comap f is trivial under $P$: every set in it has measure $0$ or $1$.

This is useful for treating an almost-surely constant observable as a null-or-conull factor in subsequent independence statements.

Original Lean declaration header

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

theorem isTrivialSigma_comap_of_ae_const [IsProbabilityMeasure P] {𝓨 : Type*}
    [MeasurableSpace 𝓨] {f : Ω → 𝓨} {y : 𝓨} (h : ∀ᵐ ω ∂P, f ω = y) :
    IsTrivialSigma P (MeasurableSpace.comap f inferInstance)

Module navigation

Module: LevyStochCalc/Probability/TrivialSigma.

Previous: IsTrivialSigma.indep.

Source excerpt, lines 51–53 · Frozen source 408915f.