Notations for probability theory #
This file defines the following notations, for functions X,Y
, measures P, Q
defined on a
measurable space m0
, and another measurable space structure m
with hm : m ≤ m0
,
P[X] = ∫ a, X a ∂P
𝔼[X] = ∫ a, X a
𝔼[X|m,hm]
: conditional expectation ofX
with respect to the measurevolume
and the measurable spacem
. The similarP[X|m,hm]
for a measureP
is defined in measure_theory.function.conditional_expectation.X =ₐₛ Y
:X =ᵐ[volume] Y
X ≤ₐₛ Y
:X ≤ᵐ[volume] Y
∂P/∂Q = P.rn_deriv Q
We note that the notation∂P/∂Q
applies to three different cases, namely,measure_theory.measure.rn_deriv
,measure_theory.signed_measure.rn_deriv
andmeasure_theory.complex_measure.rn_deriv
.
TODO: define the notation ℙ s
for the probability of a set s
, and decide whether it should be a
value in ℝ
, ℝ≥0
or ℝ≥0∞
.