English
For independent X and Y, the density of their product equals the mlconvolution of their densities.
Русский
Если X и Y независимы, плотность X·Y равна mlconvolution плотностей X и Y.
LaTeX
$$$\text{pdf}(X\cdot Y)_{\mu} =^\text{a.e.} \ pdf X_{\mu} \star_{\mu} pdf Y_{\mu}.$$$
Lean4
theorem hasFiniteIntegral_mul {f : ℝ → ℝ} {g : ℝ → ℝ≥0∞} (hg : pdf X ℙ =ᵐ[volume] g) (hgi : ∫⁻ x, ‖f x‖ₑ * g x ≠ ∞) :
HasFiniteIntegral fun x => f x * (pdf X ℙ volume x).toReal :=
by
rw [hasFiniteIntegral_iff_enorm]
have : (fun x => ‖f x‖ₑ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ :=
by
refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
refine .fun_mul (ae_eq_refl _) ?_
simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]
