Independence under a pushforward #
Two functions are independent under the pushforward of a measure along a measurable map exactly when their composites with that map are independent under the measure: the events generated by the composites are the preimages of the events generated by the functions.
Main results #
theorem
ProbabilityTheory.indepFun_map_iff_comp
{Ω : Type u_1}
{Ω' : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[MeasurableSpace Ω]
[MeasurableSpace Ω']
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
{m : Ω → Ω'}
(hm : Measurable m)
{f : Ω' → β}
{g : Ω' → γ}
(hf : Measurable f)
(hg : Measurable g)
:
Independence of two functions under a pushforward is independence of their composites.