English
Under sigma-finiteness, independence is equivalent to equality of the product map measures for the two variables.
Русский
При условия сигма-конечности независимость эквивалентна равенству произведения мер отображений для двух переменных.
LaTeX
$$$IndepFun f μ \iff μ.map f = (μ.map f) \otimes (μ.map g)$$$
Lean4
theorem indepFun_iff_map_prod_eq_prod_map_map' {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) :
IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) :=
by
rw [indepFun_iff_measure_inter_preimage_eq_mul]
have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧ μ (f ⁻¹' s ∩ g ⁻¹' t) = μ.map (fun ω ↦ (f ω, g ω)) (s ×ˢ t) :=
⟨by rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht],
(Measure.map_apply_of_aemeasurable (hf.prodMk hg) (hs.prod ht)).symm⟩
constructor
· refine fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm
rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
· intro h s t hs ht
rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
