Conditional expectation #
We build the conditional expectation of an integrable function f
with value in a Banach space
with respect to a measure μ
(defined on a measurable space structure m₀
) and a measurable space
structure m
with hm : m ≤ m₀
(a sub-sigma-algebra). This is an m
-strongly measurable
function μ[f|hm]
which is integrable and verifies ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ
for all m
-measurable sets s
. It is unique as an element of L¹
.
The construction is done in four steps:
- Define the conditional expectation of an
L²
function, as an element ofL²
. This is the orthogonal projection on the subspace of almost everywherem
-measurable functions. - Show that the conditional expectation of the indicator of a measurable set with finite measure
is integrable and define a map
Set α → (E →L[ℝ] (α →₁[μ] E))
which to a set associates a linear map. That linear map sendsx ∈ E
to the conditional expectation of the indicator of the set with valuex
. - Extend that map to
condExpL1CLM : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E)
. This is done using the same construction as the Bochner integral (see the fileMeasureTheory/Integral/SetToL1
). - Define the conditional expectation of a function
f : α → E
, which is an integrable functionα → E
equal to 0 iff
is not integrable, and equal to anm
-measurable representative ofcondExpL1CLM
applied to[f]
, the equivalence class off
inL¹
.
The first step is done in MeasureTheory.Function.ConditionalExpectation.CondexpL2
, the two
next steps in MeasureTheory.Function.ConditionalExpectation.CondexpL1
and the final step is
performed in this file.
Main results #
The conditional expectation and its properties
condExp (m : MeasurableSpace α) (μ : Measure α) (f : α → E)
: conditional expectation off
with respect tom
.integrable_condExp
:condExp
is integrable.stronglyMeasurable_condExp
:condExp
ism
-strongly-measurable.setIntegral_condExp (hf : Integrable f μ) (hs : MeasurableSet[m] s)
: ifm ≤ m₀
(the σ-algebra over which the measure is defined), then the conditional expectation verifies∫ x in s, condExp m μ f x ∂μ = ∫ x in s, f x ∂μ
for anym
-measurable sets
.
While condExp
is function-valued, we also define condExpL1
with value in L1
and a continuous
linear map condExpL1CLM
from L1
to L1
. condExp
should be used in most cases.
Uniqueness of the conditional expectation
ae_eq_condExp_of_forall_setIntegral_eq
: an a.e.m
-measurable function which verifies the equality of integrals is a.e. equal tocondExp
.
Notations #
For a measure μ
defined on a measurable space structure m₀
, another measurable space structure
m
with hm : m ≤ m₀
(a sub-σ-algebra) and a function f
, we define the notation
μ[f|m] = condExp m μ f
.
TODO #
See https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Conditional.20expectation.20of.20product
for how to prove that we can pull m
-measurable continuous linear maps out of the m
-conditional
expectation. This would generalise MeasureTheory.condExp_mul_of_stronglyMeasurable_left
.
Tags #
conditional expectation, conditional expected value
Conditional expectation of a function, with notation μ[f|m]
.
It is defined as 0 if any one of the following conditions is true:
m
is not a sub-σ-algebra ofm₀
,μ
is not σ-finite with respect tom
,f
is not integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conditional expectation of a function, with notation μ[f|m]
.
It is defined as 0 if any one of the following conditions is true:
m
is not a sub-σ-algebra ofm₀
,μ
is not σ-finite with respect tom
,f
is not integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unexpander for μ[f|m]
notation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integral of the conditional expectation μ[f|hm]
over an m
-measurable set is equal to
the integral of f
on that set.
Law of total probability using condExp
as conditional probability.
Uniqueness of the conditional expectation
If a function is a.e. m
-measurable, verifies an integrability condition and has same integral
as f
on all m
-measurable sets, then it is a.e. equal to μ[f|hm]
.
Tower property of the conditional expectation.
Taking the m₂
-conditional expectation then the m₁
-conditional expectation, where m₁
is a
smaller σ-algebra, is the same as taking the m₁
-conditional expectation directly.
Alias of MeasureTheory.MemLp.condExp
.
Lebesgue dominated convergence theorem: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
condExpL1
.
If two sequences of functions have a.e. equal conditional expectations at each step, converge and verify dominated convergence hypotheses, then the conditional expectations of their limits are a.e. equal.