English
Let f and g be two measurable functions from Ω, and κ a kernel. The pair (f,g) is independent with respect to μ and κ iff the pushforward product measure equals the product of the marginals, i.e., μ ⊗ κ.map (f,g) = μ ⊗ (κ.map f × κ.map g).
Русский
Пусть f и g — измеримые функции из Ω, κ — ядро. Независимость (f,g) относительно μ и κ эквивалентна тождеству мер: μ ⊗ κ.map (f,g) = μ ⊗ (κ.map f × κ.map g).
LaTeX
$$$\IndepFun f g κ μ \;\Leftrightarrow\; μ ⊗ κ.map (\lambda ω. (f ω, g ω)) = μ ⊗ (κ.map f \times κ.map g)$$$
Lean4
/-- Two random variables `f, g` are independent given a kernel `κ` and a measure `μ` iff
`μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)`. -/
theorem indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
[IsFiniteMeasure μ] [IsFiniteKernel κ] {f : Ω → β} {g : Ω → γ} (hf : Measurable f) (hg : Measurable g) :
IndepFun f g κ μ ↔ μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g) := by
classical
rw [indepFun_iff_measure_inter_preimage_eq_mul]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [Measure.ext_prod₃_iff]
intro u s t hu hs ht
rw [Measure.compProd_apply (hu.prod (hs.prod ht)), Measure.compProd_apply (hu.prod (hs.prod ht))]
refine lintegral_congr_ae ?_
have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
simp_rw [h_set_eq]
filter_upwards [h s t hs ht] with ω hω
by_cases hωu : ω ∈ u
swap; · simp [hωu]
simp only [hωu, ↓reduceIte]
rw [map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht), mk_preimage_prod, hω, prod_apply_prod,
map_apply' _ (by fun_prop), map_apply' _ (by fun_prop)]
exacts [ht, hs]
· intro s t hs ht
rw [Measure.ext_prod₃_iff] at h
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
· exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))
· exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))
intro u hu hμu
specialize h hu hs ht
rw [Measure.compProd_apply_prod hu (hs.prod ht), Measure.compProd_apply_prod hu (hs.prod ht)] at h
convert h with ω ω
· rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
· rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]
