English
The independence of a family X_i of random variables is equivalent to the equality of the joint distribution μ ∘ X with the infinite product of their marginals, provided each X_i is measurable.
Русский
Независимость семейства X_i эквивалентна равенству совместного распределения и бесконечного произведения маргиналов при условии измеримости каждого X_i.
LaTeX
$$$\text{If } (X_i)_{i\in ι} \text{ are measurable} \,:\; iIndepFun X μ \iff μ.map (λ ω i. X_i ω) = infinitePi (λ i. μ.map (X_i)).$$$
Lean4
/-- Random variables are independent iff their joint distribution is the product measure. This
is a version where the random variable `ω ↦ (Xᵢ(ω))ᵢ` is almost everywhere measurable.
See `iIndepFun_iff_map_fun_eq_infinitePi_map₀'` for a version which only assumes that
each `Xᵢ` is almost everywhere measurable and that `ι` is countable. -/
theorem iIndepFun_iff_map_fun_eq_infinitePi_map₀ (mX : AEMeasurable (fun ω i ↦ X i ω) μ) :
haveI _ i := isProbabilityMeasure_map (mX.eval i)
iIndepFun X μ ↔ μ.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ μ.map (X i))
where
mp
h := by
have _ i := isProbabilityMeasure_map (mX.eval i)
refine eq_infinitePi _ fun s t ht ↦ ?_
rw [iIndepFun_iff_finset] at h
have : s.toSet.pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t i) := by ext; simp
rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
· have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
rw [this, (iIndepFun_iff_map_fun_eq_pi_map ?_).1 (h s), pi_pi]
· simp only [Finset.restrict]
rw [s.prod_coe_sort fun i ↦ μ.map (X i) (t i)]
exact fun i ↦ mX.eval i
any_goals fun_prop
· exact mX
· exact .univ_pi fun i ↦ ht i i.2
mpr
h := by
rw [iIndepFun_iff_finset]
intro s
rw [iIndepFun_iff_map_fun_eq_pi_map]
· have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]
· simp
· fun_prop
exact mX
exact fun i ↦ mX.eval i
