English
If a set of events is conditionally independent, then the associated indicator-valued functions are conditionally independent when mapped into the product space.
Русский
Если множество событий условно независимо, то соответствующие индикаторные функции независимы в произведении пространства.
LaTeX
$$$[Zero\; β] [One\; β] \Rightarrow (hs : iCondIndepSet m' hm' s μ) \Rightarrow iCondIndepFun m' hm' (fun n => (s n).indicator (\lambda _ => 1)) μ$$$
Lean4
/-- If `f` and `g` with values in `ℝ≥0∞` are independent and almost everywhere measurable,
then `E[f * g] = E[f] * E[g]` (slightly generalizing
`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun`). -/
theorem lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' (h_meas_f : AEMeasurable f μ)
(h_meas_g : AEMeasurable g μ) (h_indep_fun : IndepFun f g μ) :
(∫⁻ ω, (f * g) ω ∂μ) = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, g ω ∂μ :=
by
have fg_ae : f * g =ᵐ[μ] h_meas_f.mk _ * h_meas_g.mk _ := h_meas_f.ae_eq_mk.mul h_meas_g.ae_eq_mk
rw [lintegral_congr_ae h_meas_f.ae_eq_mk, lintegral_congr_ae h_meas_g.ae_eq_mk, lintegral_congr_ae fg_ae]
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun h_meas_f.measurable_mk h_meas_g.measurable_mk
exact h_indep_fun.congr h_meas_f.ae_eq_mk h_meas_g.ae_eq_mk
