English
If two functions X and Y are independent random variables with values in a normed division ring, then their product is integrable if both are integrable.
Русский
Если X и Y независимые, то произведение интегрируемо, если оба интегрируемы.
LaTeX
$$$\text{IndepFun } X Y μ \Rightarrow \text{Integrable } X μ \land \text{Integrable } Y μ \Rightarrow \text{Integrable } (X Y) μ$$$
Lean4
/-- If a random variable `f` in `ℝ≥0∞` is independent of an event `T`, then if you restrict the
random variable to `T`, then `E[f * indicator T c 0]=E[f] * E[indicator T c 0]`. It is useful for
`lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace`. -/
theorem lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator {Mf mΩ : MeasurableSpace Ω} {μ : Measure Ω}
(hMf : Mf ≤ mΩ) (c : ℝ≥0∞) {T : Set Ω} (h_meas_T : MeasurableSet T)
(h_ind : IndepSets {s | MeasurableSet[Mf] s} { T } μ) (h_meas_f : Measurable[Mf] f) :
(∫⁻ ω, f ω * T.indicator (fun _ => c) ω ∂μ) = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, T.indicator (fun _ => c) ω ∂μ :=
by
revert f
have h_mul_indicator : ∀ g, Measurable g → Measurable fun a => g a * T.indicator (fun _ => c) a := fun g h_mg =>
h_mg.mul (measurable_const.indicator h_meas_T)
apply @Measurable.ennreal_induction _ Mf
· intro c' s' h_meas_s'
simp_rw [← inter_indicator_mul]
rw [lintegral_indicator (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T), lintegral_indicator (hMf _ h_meas_s'),
lintegral_indicator h_meas_T]
simp only [lintegral_const, univ_inter, MeasurableSet.univ, Measure.restrict_apply]
rw [IndepSets_iff] at h_ind
rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]
· intro f' g _ h_meas_f' _ h_ind_f' h_ind_g
have h_measM_f' : Measurable f' := h_meas_f'.mono hMf le_rfl
simp_rw [Pi.add_apply, right_distrib]
rw [lintegral_add_left (h_mul_indicator _ h_measM_f'), lintegral_add_left h_measM_f', right_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 hMf le_rfl
simp_rw [ENNReal.iSup_mul]
rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, ENNReal.iSup_mul]
· simp_rw [← h_ind_f]
· exact fun n => h_mul_indicator _ (h_measM_f n)
· exact fun m n h_le a => mul_le_mul_right' (h_mono_f h_le a) _
