English
Two random variables X_i are independent iff their joint characteristic function equals the product of their marginals' characteristic functions in the WithLp framework.
Русский
Две случайные величины независимы тогда и только тогда, когда их совместная характеристическая функция равна произведению характерфункций marginals в рамках WithLp.
LaTeX
$$$IndepFun(X,Y,μ) \\iff \\forall t, charFun(μ map (X,Y)) = \\, charFun(μ map X) \\cdot charFun(μ map Y)$$$
Lean4
theorem condIndepSets_iff (s1 s2 : Set (Set Ω)) (hs1 : ∀ s ∈ s1, MeasurableSet s) (hs2 : ∀ s ∈ s2, MeasurableSet s)
(μ : Measure Ω) [IsFiniteMeasure μ] :
CondIndepSets m' hm' s1 s2 μ ↔
∀ (t1 t2 : Set Ω) (_ : t1 ∈ s1) (_ : t2 ∈ s2), (μ⟦t1 ∩ t2|m'⟧) =ᵐ[μ] (μ⟦t1|m'⟧) * (μ⟦t2|m'⟧) :=
by
simp only [CondIndepSets, Kernel.IndepSets]
have hs1_eq : ∀ s ∈ s1, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s|m'⟧ := fun s hs ↦
condExpKernel_ae_eq_condExp hm' (hs1 s hs)
have hs2_eq : ∀ s ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s|m'⟧ := fun s hs ↦
condExpKernel_ae_eq_condExp hm' (hs2 s hs)
have hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (s ∩ t))) =ᵐ[μ] μ⟦s ∩ t|m'⟧ :=
fun s hs t ht ↦ condExpKernel_ae_eq_condExp hm' ((hs1 s hs).inter ((hs2 t ht)))
refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩ <;> specialize h s t hs ht
· have h' := ae_eq_of_ae_eq_trim h
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h'] with ω hs_eq ht_eq hst_eq h'
rw [← hst_eq, Pi.mul_apply, ← hs_eq, ← ht_eq, h', ENNReal.toReal_mul]
· refine
((stronglyMeasurable_condExpKernel ((hs1 s hs).inter (hs2 t ht))).ae_eq_trim_iff hm'
((measurable_condExpKernel (hs1 s hs)).mul (measurable_condExpKernel (hs2 t ht))).stronglyMeasurable).mpr
?_
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h] with ω hs_eq ht_eq hst_eq h
have h_ne_top : condExpKernel μ m' ω (s ∩ t) ≠ ∞ := measure_ne_top (condExpKernel μ m' ω) _
rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq, ← ENNReal.toReal_mul,
ENNReal.ofReal_toReal]
exact ENNReal.mul_ne_top (measure_ne_top (condExpKernel μ m' ω) s) (measure_ne_top (condExpKernel μ m' ω) t)
