Integration in Probability Theory #

Integration results for independent random variables. Specifically, for two independent random variables X and Y over the extended non-negative reals, E[X * Y] = E[X] * E[Y], and similar results.

source

theorem probability_theory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator {α : Type u_1} {Mf : measurable_space α} [M : measurable_space α] {μ : measure_theory.measure α} (hMf : Mf ≤ M) (c : ℝ≥0∞) {T : set α} (h_meas_T : M.measurable_set' T) (h_ind : probability_theory.indep_sets Mf.measurable_set' {T} μ) {f : α → ℝ≥0∞} (h_meas_f : measurable f) :

∫⁻ (a : α), (f a) * T.indicator (λ (_x : α), c) a ∂μ = (∫⁻ (a : α), f a ∂μ) * ∫⁻ (a : α), T.indicator (λ (_x : α), c) a ∂μ

This (roughly) proves that if a random variable f is independent of an event T, then if you restrict the random variable to T, then E[f * indicator T c 0]=E[f] * E[indicator T c 0]. It is useful for lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space.

source

theorem probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space {α : Type u_1} {Mf Mg : measurable_space α} [M : measurable_space α] {μ : measure_theory.measure α} (hMf : Mf ≤ M) (hMg : Mg ≤ M) (h_ind : probability_theory.indep Mf Mg μ) (f g : α → ℝ≥0∞) (h_meas_f : measurable f) (h_meas_g : measurable g) :

∫⁻ (a : α), (f a) * g a ∂μ = (∫⁻ (a : α), f a ∂μ) * ∫⁻ (a : α), g a ∂μ

This (roughly) proves that if f and g are independent random variables, then E[f * g] = E[f] * E[g]. However, instead of directly using the independence of the random variables, it uses the independence of measurable spaces for the domains of f and g. This is similar to the sigma-algebra approach to independence. See lintegral_mul_eq_lintegral_mul_lintegral_of_independent_fn for a more common variant of the product of independent variables.

source

theorem probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun {α : Type u_1} [M : measurable_space α] (μ : measure_theory.measure α) (f g : α → ℝ≥0∞) (h_meas_f : measurable f) (h_meas_g : measurable g) (h_indep_fun : probability_theory.indep_fun (borel ℝ≥0∞) (borel ℝ≥0∞) f g μ) :

∫⁻ (a : α), (f * g) a ∂μ = (∫⁻ (a : α), f a ∂μ) * ∫⁻ (a : α), g a ∂μ

This proves that if f and g are independent random variables, then E[f * g] = E[f] * E[g].