English
Equivalence between conditional independence of functions and a product-of-conditional-expectations statement over finite index sets.
Русский
Эквивалентность условной независимости функций и произведения условных ожиданий над конечными подмножествами индексов.
LaTeX
$$$\text{iCondIndepFun } m' hm' f g \mu \iff\ \forall S,\ \{sets_i\},\ (\forall i, i\in S \to MeasurableSet(sets_i))\ \Rightarrow\ (\mu\text{⟮⋂}_{i\in S} f_i^{-1}(sets_i)|m') =^\ast_{\mu} \prod_{i\in S} (\mu\text{⟮f_i^{-1}(sets_i)}/m')$$$
Lean4
theorem iCondIndepFun_iff_condExp_inter_preimage_eq_mul {β : ι → Type*} (m : ∀ x, MeasurableSpace (β x))
(f : ∀ i, Ω → β i) (hf : ∀ i, Measurable (f i)) :
iCondIndepFun m' hm' f μ ↔
∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
(μ⟦⋂ i ∈ S, f i ⁻¹' sets i|m'⟧) =ᵐ[μ] ∏ i ∈ S, (μ⟦f i ⁻¹' sets i|m'⟧) :=
by
rw [iCondIndepFun_iff]
swap
· exact hf
refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
· refine h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)
exact ⟨sets i, h_sets i hi, rfl⟩
·
classical
let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
specialize h s (sets := g) (fun i hi ↦ ?_)
· simp only [g, dif_pos hi]
exact (h_sets i hi).choose_spec.1
· have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
intro i hi
rw [(h_sets i hi).choose_spec.2.symm]
simp only [g, dif_pos hi]
convert h with i hi i hi <;> exact hg i hi
