English
Conditionally independent family: iCondIndepSets m' hm' π μ is equivalent to an equality of conditional set probabilities across finite index sets.
Русский
Условно независимое семейство: iCondIndepSets эквивалентно равенству условий распределения по конечным индексам.
LaTeX
$$$iCondIndepSets(m',hm',\\pi,\\mu)\\iff \\forall S, \\cdots: \\text{[conditional products]}$$$
Lean4
theorem iCondIndepSets_singleton_iff (s : ι → Set Ω) (hπ : ∀ i, MeasurableSet (s i)) (μ : Measure Ω)
[IsFiniteMeasure μ] :
iCondIndepSets m' hm' (fun i ↦ {s i}) μ ↔ ∀ S : Finset ι, μ⟦⋂ i ∈ S, s i|m'⟧ =ᵐ[μ] ∏ i ∈ S, (μ⟦s i|m'⟧) :=
by
rw [iCondIndepSets_iff]
· simp only [Set.mem_singleton_iff]
refine ⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩
filter_upwards [h S] with a ha
refine Eq.trans ?_ (ha.trans ?_)
· grind
· simp_rw [Finset.prod_apply]
refine Finset.prod_congr rfl (fun i hi ↦ ?_)
rw [hf i hi]
· simpa only [Set.mem_singleton_iff, forall_eq]
