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 MeasurableSpace
M2
to define μ
:
example {M1 : MeasurableSpace Ω} [M2 : MeasurableSpace Ω] {μ : Measure Ω} : sorry := sorry
example [M1 : MeasurableSpace Ω] {M2 : MeasurableSpace Ω} {μ : Measure Ω} : sorry := sorry
If a random variable f
in ℝ≥0∞
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_measurableSpace
.
If f
and g
are independent random variables with values in ℝ≥0∞
,
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_indepFun
for
a more common variant of the product of independent variables.
If f
and g
are independent random variables with values in ℝ≥0∞
,
then E[f * g] = E[f] * E[g]
.
If f
and g
with values in ℝ≥0∞
are independent and almost everywhere measurable,
then E[f * g] = E[f] * E[g]
(slightly generalizing
lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun
).
The product of two independent, integrable, real-valued random variables is integrable.
If the product of two independent real-valued random variables is integrable and the second one is not almost everywhere zero, then the first one is integrable.
If the product of two independent real-valued random variables is integrable and the first one is not almost everywhere zero, then the second one is integrable.
Alias of ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
.
Alias of ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
.
Alias of ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
.
Alias of ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral
.
Independence of functions f
and g
into arbitrary types is characterized by the relation
E[(φ ∘ f) * (ψ ∘ g)] = E[φ ∘ f] * E[ψ ∘ g]
for all measurable φ
and ψ
with values in ℝ
satisfying appropriate integrability conditions.