English
If X and Y are independent random variables and X, Y are measurable with respect to appropriately mapped measures, then the integral of a product composition equals the product of the integrals.
Русский
Если X, Y независимы и измеримы относительно соответствующих отображений мер, то интеграл произведения композиции равен произведению интегралов.
LaTeX
$$$\text{IndepFun } X Y μ \Rightarrow \text{AEMeasurable } X μ \Rightarrow \text{AEMeasurable } Y μ \Rightarrow \int f(X)\,dμ \cdot \int g(Y)\,dμ = \int (f(X) g(Y)) dμ$$$
Lean4
theorem integral_fun_comp_mul_comp {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {X : Ω → 𝓧}
{Y : Ω → 𝓨} {f : 𝓧 → 𝕜} {g : 𝓨 → 𝕜} (hXY : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
(hf : AEStronglyMeasurable f (μ.map X)) (hg : AEStronglyMeasurable g (μ.map Y)) :
∫ ω, f (X ω) * g (Y ω) ∂μ = (∫ ω, f (X ω) ∂μ) * ∫ ω, g (Y ω) ∂μ :=
by
have hfXgY := (hXY.comp₀ hX hY hf.aemeasurable hg.aemeasurable)
have hfX := (hf.comp_aemeasurable hX)
have hgY := (hg.comp_aemeasurable hY)
by_cases h'X : ∀ᵐ ω ∂μ, f (X ω) = 0
· have h' : ∀ᵐ ω ∂μ, f (X ω) * g (Y ω) = 0 :=
by
filter_upwards [h'X] with ω hω
simp [hω]
simp [integral_congr_ae h'X, integral_congr_ae h']
by_cases h'Y : ∀ᵐ ω ∂μ, g (Y ω) = 0
· have h' : ∀ᵐ ω ∂μ, f (X ω) * g (Y ω) = 0 :=
by
filter_upwards [h'Y] with ω hω
simp [hω]
simp [integral_congr_ae h'Y, integral_congr_ae h']
by_cases h : Integrable (fun ω ↦ f (X ω) * g (Y ω)) μ
· have := (hfXgY.integrable_left_of_integrable_mul h hfX hgY h'Y).isProbabilityMeasure_of_indepFun _ _ h'X hfXgY
change ∫ ω, (fun x ↦ f x.1 * g x.2) (X ω, Y ω) ∂μ = _
rw [← integral_map (f := fun x ↦ f x.1 * g x.2) (φ := fun ω ↦ (X ω, Y ω)),
(indepFun_iff_map_prod_eq_prod_map_map hX hY).1 hXY, integral_prod_mul, integral_map, integral_map]
any_goals fun_prop
rw [(indepFun_iff_map_prod_eq_prod_map_map hX hY).1 hXY]
exact hf.comp_fst.mul hg.comp_snd
· rw [integral_undef h]
obtain h | h : ¬(Integrable (fun ω ↦ f (X ω)) μ) ∨ ¬(Integrable (fun ω ↦ g (Y ω)) μ) :=
not_and_or.1 fun ⟨HX, HY⟩ ↦ h (hfXgY.integrable_mul HX HY)
all_goals simp [integral_undef h]
