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.

Implementation notes #

Many lemmas in this file take two arguments of the same typeclass. It is worth remembering that lean will always pick the later typeclass in this situation, and does not care whether the arguments are [], {}, or (). All of these use the measurable_space M2 to define μ:

example {M1 : measurable_space α} [M2 : measurable_space α] {μ : measure α} : sorry := sorry
example [M1 : measurable_space α] {M2 : measurable_space α} {μ : measure α} : sorry := sorry

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 : 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} [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 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].