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).
If X and Y are two independent and integrable random variables, and B is a function of
two variables such that ‖B x y‖ₑ ≤ C * ‖x‖ₑ * ‖y‖ₑ, then B X Y is integrable.
This is useful in particular if B is a continuous bilinear map.
A continuous bilinear map applied to two independent and integrable random variables is integrable.
If X and Y are two independent random variables, B X Y is integrable, Y is not
almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then X is integrable.
This is useful for the case where B is scalar multiplication, as it will allow to drop
integrability hypotheses.
If X and Y are two independent random variables, B X Y is integrable, X is not
almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then Y is integrable.
This is useful for the case where B is scalar multiplication, as it will allow to drop
integrability hypotheses.
If X and Y are independent random variables such that f(X) and g(Y) are integrable
and B is a continuous bilinear map, then
∫ ω, B (f (X ω)) (g (Y ω)) ∂μ = B (∫ ω, f (X ω) ∂μ) (∫ ω, g (Y ω) ∂μ).
If X and Y are random variables and B is a continuous bilinear map
such that ∀ x y, c * ‖x‖ * ‖y‖ ≤ ‖B x y‖, then
∫ ω, B (f (X ω)) (g (Y ω)) ∂μ = B (∫ ω, f (X ω) ∂μ) (∫ ω, g (Y ω) ∂μ).
The assumption on B allows to drop the integrability condition in
IndepFun.integral_bilin_comp_comp, which is useful for the versions where B is the scalar
multiplication or the multiplication.
If X and Y are independent and integrable random variables and B
is a continuous bilinear map, then ∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y].
If X and Y are random variables and B is a continuous bilinear map
such that ∀ x y, c * ‖x‖ * ‖y‖ ≤ ‖B x y‖, then ∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y].
The assumption on B allows to drop the integrability condition in
IndepFun.integral_bilin', which is useful for the versions where B is the scalar
multiplication or the multiplication.
The scalar product of two independent and integrable random variables is integrable.
The product of two independent and integrable random variables is integrable.
Alias of ProbabilityTheory.IndepFun.integrable_left_of_integrable_op.
If X and Y are two independent random variables, B X Y is integrable, Y is not
almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then X is integrable.
This is useful for the case where B is scalar multiplication, as it will allow to drop
integrability hypotheses.
Alias of ProbabilityTheory.IndepFun.integrable_right_of_integrable_op.
If X and Y are two independent random variables, B X Y is integrable, X is not
almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then Y is integrable.
This is useful for the case where B is scalar multiplication, as it will allow to drop
integrability hypotheses.
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.