English
If sets s_n are independent in the iIndepSet sense, then the indicator functions of s_n, viewed as random integers 1 on s_n and 0 elsewhere, are independent as a family of random variables.
Русский
Если множества s_n независимы в смысле iIndepSet, то индикаторные функции 1 на s_n и 0 вне с ними образуют независимое семейство случайных величин.
LaTeX
$$$\\text{iIndepFun}\\left(n \\mapsto (s_n).indicator 1\\right)\\kappa\\mu$$$
Lean4
theorem iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β} {s : ι → Set Ω} (hs : iIndepSet s κ μ) :
iIndepFun (fun n => (s n).indicator fun _ω => (1 : β)) κ μ := by
classical
rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
rintro S π _hπ
simp_rw [Set.indicator_const_preimage_eq_union]
apply hs _ fun i _hi ↦ ?_
have hsi : MeasurableSet[generateFrom {s i}] (s i) := measurableSet_generateFrom (Set.mem_singleton _)
refine
MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
(MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
· exact @MeasurableSet.empty _ (generateFrom {s i})
· exact @MeasurableSet.empty _ (generateFrom {s i})
