IndependenceMap #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Independence under a pushforward measure #
This file relates independence of two sigma-fields pulled back along a map to independence of the original sigma-fields under the pushforward measure.
Main results #
indep_comap_iff_indep_map: independence of two comap sigma-fields is equivalent to independence under the pushforward measure.
theorem
Algsuperdiff.Probability.indep_comap_iff_indep_map
{α : Type u_1}
{β : Type u_2}
[mAlpha : MeasurableSpace α]
{m₁ m₂ : MeasurableSpace β}
[mBeta : MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(hm₁ : m₁ ≤ mBeta)
(hm₂ : m₂ ≤ mBeta)
:
ProbabilityTheory.Indep (MeasurableSpace.comap f m₁) (MeasurableSpace.comap f m₂) μ ↔ ProbabilityTheory.Indep m₁ m₂ (MeasureTheory.Measure.map f μ)
Two sigma-fields pulled back along an almost-everywhere measurable map are independent exactly when the original sigma-fields are independent under the pushforward measure. The sigma-fields on the target must be contained in its ambient measurable space so that the pushforward can be evaluated on all of their events.