English
The product of two independent integrable random variables is integrable.
Русский
Произведение двух независимых интегрируемых случайных величин интегрируемо.
LaTeX
$$$\text{IndepFun } X Y μ \Rightarrow \text{Integrable } X μ \land \text{Integrable } Y μ \Rightarrow \text{Integrable } (X \cdot Y) μ$$$
Lean4
/-- The product of two independent, integrable, real-valued random variables is integrable. -/
theorem integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β} [NormedDivisionRing β] [BorelSpace β]
(hXY : IndepFun X Y μ) (hX : Integrable X μ) (hY : Integrable Y μ) : Integrable (X * Y) μ :=
by
let nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
let nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
have hXY' : IndepFun nX nY μ := hXY.comp measurable_enorm measurable_enorm
have hnX : AEMeasurable nX μ := hX.1.aemeasurable.enorm
have hnY : AEMeasurable nY μ := hY.1.aemeasurable.enorm
have hmul : ∫⁻ a, nX a * nY a ∂μ = (∫⁻ a, nX a ∂μ) * ∫⁻ a, nY a ∂μ :=
lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' hnX hnY hXY'
refine ⟨hX.1.mul hY.1, ?_⟩
simp only [nX, nY] at hmul
simp_rw [hasFiniteIntegral_iff_enorm, Pi.mul_apply, enorm_mul, hmul]
exact ENNReal.mul_lt_top hX.2 hY.2
