English
If f is integrable and independent of an event T, then the lintegral of f times the indicator of T is the product of the lintegral of f with the lintegral of the indicator of T.
Русский
Если f интегрируема и независима от T, то ∫ f · 1_T = ∫ f · ∫ 1_T.
LaTeX
$$$\int f \cdot T.indicator(c) = (\int f) (\int T.indicator(c))$$$
Lean4
/-- If `f` and `g` are independent random variables with values in `ℝ≥0∞`,
then `E[f * g] = E[f] * E[g]`. However, instead of directly using the independence
of the random variables, it uses the independence of measurable spaces for the
domains of `f` and `g`. This is similar to the sigma-algebra approach to
independence. See `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun` for
a more common variant of the product of independent variables. -/
theorem lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace {Mf Mg mΩ : MeasurableSpace Ω}
{μ : Measure Ω} (hMf : Mf ≤ mΩ) (hMg : Mg ≤ mΩ) (h_ind : Indep Mf Mg μ) (h_meas_f : Measurable[Mf] f)
(h_meas_g : Measurable[Mg] g) : ∫⁻ ω, f ω * g ω ∂μ = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, g ω ∂μ :=
by
revert g
have h_measM_f : Measurable f := h_meas_f.mono hMf le_rfl
apply @Measurable.ennreal_induction _ Mg
· intro c s h_s
apply lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator hMf _ (hMg _ h_s) _ h_meas_f
apply indepSets_of_indepSets_of_le_right h_ind
rwa [singleton_subset_iff]
· intro f' g _ h_measMg_f' _ h_ind_f' h_ind_g'
have h_measM_f' : Measurable f' := h_measMg_f'.mono hMg le_rfl
simp_rw [Pi.add_apply, left_distrib]
rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib, h_ind_f', h_ind_g']
· intro f' h_meas_f' h_mono_f' h_ind_f'
have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
simp_rw [ENNReal.mul_iSup]
rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', ENNReal.mul_iSup]
· simp_rw [← h_ind_f']
· exact fun n => h_measM_f.mul (h_measM_f' n)
· exact fun n m (h_le : n ≤ m) a => mul_le_mul_left' (h_mono_f' h_le a) _
