lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun

English

If X_i are independent in the sense of IndepFun, then the product of a finite subset is independent of another finite product collection, provided appropriate measurability.

Русский

Если X_i независимы, то произведение некоторых из них независимо от произведения других, при соблюдении измеримости.

LaTeX

$$$\forall s,t \subseteq ι, \; s \cap t = \emptyset \Rightarrow \; (\prod_{i\in s} X_i) \perp (\prod_{j\in t} X_j)$$$

Lean4

/-- If `f` and `g` are independent random variables with values in `ℝ≥0∞`,
then `E[f * g] = E[f] * E[g]`. -/
theorem lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun (h_meas_f : Measurable f) (h_meas_g : Measurable g)
    (h_indep_fun : IndepFun f g μ) : (∫⁻ ω, (f * g) ω ∂μ) = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, g ω ∂μ :=
  lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace (measurable_iff_comap_le.1 h_meas_f)
    (measurable_iff_comap_le.1 h_meas_g) h_indep_fun (Measurable.of_comap_le le_rfl) (Measurable.of_comap_le le_rfl)

Похожие утверждения