English
If X and Y are independent under μ, then exp(sX) and exp(tY) are independent under μ for any real s,t.
Русский
Если X и Y независимы относительно μ, то exp(sX) и exp(tY) независимы относительно μ для любых действительных s,t.
LaTeX
$$$\text{If } \mathrm{IndepFun}(X,Y,\mu)\text{ then } \mathrm{IndepFun}\big(\lambda \omega. e^{sX(\omega)}, \lambda \omega. e^{tY(\omega)}, \mu\big).$$$
Lean4
/-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
theorem exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ :=
by
have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp
change IndepFun ((fun x => exp (s * x)) ∘ X) ((fun x => exp (t * x)) ∘ Y) μ
exact IndepFun.comp h_indep (h_meas s) (h_meas t)
