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 m0
) and a measurable space
structure m
with hm : m ≤ m0
(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
condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E)
. This is done using the same construction as the Bochner integral (see the filemeasure_theory/integral/set_to_L1
). - 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 ofcondexp_L1_clm
applied to[f]
, the equivalence class off
inL¹
.
Main results #
The conditional expectation and its properties
condexp (m : measurable_space α) (μ : measure α) (f : α → E)
: conditional expectation off
with respect tom
.integrable_condexp
:condexp
is integrable.strongly_measurable_condexp
:condexp
ism
-strongly-measurable.set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s)
: ifm ≤ m0
(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 condexp_L1
with value in L1
and a continuous
linear map condexp_L1_clm
from L1
to L1
. condexp
should be used in most cases.
Uniqueness of the conditional expectation
Lp.ae_eq_of_forall_set_integral_eq'
: twoLp
functions verifying the equality of integrals defining the conditional expectation are equal.ae_eq_of_forall_set_integral_eq_of_sigma_finite'
: two functions verifying the equality of integrals defining the conditional expectation are equal almost everywhere. Requires[sigma_finite (μ.trim hm)]
.ae_eq_condexp_of_forall_set_integral_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 m0
, another measurable space structure
m
with hm : m ≤ m0
(a sub-σ-algebra) and a function f
, we define the notation
μ[f|m] = condexp m μ f
.
Implementation notes #
Most of the results in this file are valid for a complete real normed space F
.
However, some lemmas also use 𝕜 : is_R_or_C
:
condexp_L2
is defined only for aninner_product_space
for now, and we use𝕜
for its field.- results about scalar multiplication are stated not only for
ℝ
but also for𝕜
if we happen to havenormed_space 𝕜 F
.
Tags #
conditional expectation, conditional expected value
A function f
verifies ae_strongly_measurable' m f μ
if it is μ
-a.e. equal to
an m
-strongly measurable function. This is similar to ae_strongly_measurable
, but the
measurable_space
structures used for the measurability statement and for the measure are
different.
Equations
- measure_theory.ae_strongly_measurable' m f μ = ∃ (g : α → β), measure_theory.strongly_measurable g ∧ f =ᵐ[μ] g
An m
-strongly measurable function almost everywhere equal to f
.
Equations
If the restriction to a set s
of a σ-algebra m
is included in the restriction to s
of
another σ-algebra m₂
(hypothesis hs
), the set s
is m
measurable and a function f
almost
everywhere supported on s
is m
-ae-strongly-measurable, then f
is also
m₂
-ae-strongly-measurable.
The subset Lp_meas
of Lp
functions a.e. measurable with respect to a sub-sigma-algebra #
Lp_meas_subgroup F m p μ
is the subspace of Lp F p μ
containing functions f
verifying
ae_strongly_measurable' m f μ
, i.e. functions which are μ
-a.e. equal to
an m
-strongly measurable function.
Equations
- measure_theory.Lp_meas_subgroup F m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥measure_theory.Lp_meas_subgroup
Lp_meas F 𝕜 m p μ
is the subspace of Lp F p μ
containing functions f
verifying
ae_strongly_measurable' m f μ
, i.e. functions which are μ
-a.e. equal to
an m
-strongly measurable function.
Equations
- measure_theory.Lp_meas F 𝕜 m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for ↥measure_theory.Lp_meas
The subspace Lp_meas
is complete. #
We define an isometry_equiv
between Lp_meas_subgroup
and the Lp
space corresponding to the
measure μ.trim hm
. As a consequence, the completeness of Lp
implies completeness of
Lp_meas_subgroup
(and Lp_meas
).
If f
belongs to Lp_meas_subgroup F m p μ
, then the measurable function it is almost
everywhere equal to (given by ae_measurable.mk
) belongs to ℒp
for the measure μ.trim hm
.
If f
belongs to Lp
for the measure μ.trim hm
, then it belongs to the subgroup
Lp_meas_subgroup F m p μ
.
Map from Lp_meas_subgroup
to Lp F p (μ.trim hm)
.
Equations
Map from Lp_meas
to Lp F p (μ.trim hm)
.
Equations
- measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f = measure_theory.mem_ℒp.to_Lp (Exists.some _) _
Map from Lp F p (μ.trim hm)
to Lp_meas_subgroup
, inverse of
Lp_meas_subgroup_to_Lp_trim
.
Equations
- measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
Map from Lp F p (μ.trim hm)
to Lp_meas
, inverse of Lp_meas_to_Lp_trim
.
Equations
- measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
Lp_trim_to_Lp_meas_subgroup
is a right inverse of Lp_meas_subgroup_to_Lp_trim
.
Lp_trim_to_Lp_meas_subgroup
is a left inverse of Lp_meas_subgroup_to_Lp_trim
.
Lp_meas_subgroup_to_Lp_trim
preserves the norm.
Lp_meas_subgroup
and Lp F p (μ.trim hm)
are isometric.
Equations
- measure_theory.Lp_meas_subgroup_to_Lp_trim_iso F p μ hm = {to_equiv := {to_fun := measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm, inv_fun := measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm, left_inv := _, right_inv := _}, isometry_to_fun := _}
Lp_meas_subgroup
and Lp_meas
are isometric.
Equations
Lp_meas
and Lp F p (μ.trim hm)
are isometric, with a linear equivalence.
Equations
- measure_theory.Lp_meas_to_Lp_trim_lie F 𝕜 p μ hm = {to_linear_equiv := {to_fun := measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm, map_add' := _, map_smul' := _, inv_fun := measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm, left_inv := _, right_inv := _}, norm_map' := _}
We do not get ae_fin_strongly_measurable f (μ.trim hm)
, since we don't have
f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f
but only the weaker
f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f
.
When applying the inverse of Lp_meas_to_Lp_trim_lie
(which takes a function in the Lp space of
the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the
sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra.
Auxiliary lemma for Lp.induction_strongly_measurable
.
To prove something for an Lp
function a.e. strongly measurable with respect to a
sub-σ-algebra m
in a normed space, it suffices to show that
- the property holds for (multiples of) characteristic functions which are measurable w.r.t.
m
; - is closed under addition;
- the set of functions in
Lp
strongly measurable w.r.t.m
for which the property holds is closed.
To prove something for an arbitrary mem_ℒp
function a.e. strongly measurable with respect
to a sub-σ-algebra m
in a normed space, it suffices to show that
- the property holds for (multiples of) characteristic functions which are measurable w.r.t.
m
; - is closed under addition;
- the set of functions in the
Lᵖ
space strongly measurable w.r.t.m
for which the property holds is closed. - the property is closed under the almost-everywhere equal relation.
Uniqueness of the conditional expectation #
Uniqueness of the conditional expectation
Let m
be a sub-σ-algebra of m0
, f
a m0
-measurable function and g
a m
-measurable
function, such that their integrals coincide on m
-measurable sets with finite measure.
Then ∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ
on all m
-measurable sets with finite measure.
Let m
be a sub-σ-algebra of m0
, f
a m0
-measurable function and g
a m
-measurable
function, such that their integrals coincide on m
-measurable sets with finite measure.
Then ∫⁻ x in s, ‖g x‖₊ ∂μ ≤ ∫⁻ x in s, ‖f x‖₊ ∂μ
on all m
-measurable sets with finite
measure.
Conditional expectation in L2 #
We define a conditional expectation in L2
: it is the orthogonal projection on the subspace
Lp_meas
.
Conditional expectation of a function in L2 with respect to a sigma-algebra
Equations
- measure_theory.condexp_L2 𝕜 hm = orthogonal_projection (measure_theory.Lp_meas E 𝕜 m 2 μ)
condexp_L2
commutes with taking inner products with constants. See the lemma
condexp_L2_comp_continuous_linear_map
for a more general result about commuting with continuous
linear maps.
condexp_L2
verifies the equality of integrals defining the conditional expectation.
If the measure μ.trim hm
is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
Conditional expectation of the indicator of a measurable set with finite measure, in L2.
Equations
- measure_theory.condexp_ind_smul hm hs hμs x = ⇑(continuous_linear_map.comp_LpL 2 μ (continuous_linear_map.to_span_singleton ℝ x)) ↑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
If the measure μ.trim hm
is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
Conditional expectation of an indicator as a continuous linear map. #
The goal of this section is to build
condexp_ind (hm : m ≤ m0) (μ : measure α) (s : set s) : G →L[ℝ] α →₁[μ] G
, which
takes x : G
to the conditional expectation of the indicator of the set s
with value x
,
seen as an element of α →₁[μ] G
.
Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.
Equations
- measure_theory.condexp_ind_L1_fin hm hs hμs x = measure_theory.integrable.to_L1 ⇑(measure_theory.condexp_ind_smul hm hs hμs x) _
Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.
Equations
- measure_theory.condexp_ind_L1 hm μ s x = dite (measurable_set s ∧ ⇑μ s ≠ ⊤) (λ (hs : measurable_set s ∧ ⇑μ s ≠ ⊤), measure_theory.condexp_ind_L1_fin hm _ _ x) (λ (hs : ¬(measurable_set s ∧ ⇑μ s ≠ ⊤)), 0)
Conditional expectation of the indicator of a set, as a linear map from G
to L1.
Equations
- measure_theory.condexp_ind hm μ s = {to_linear_map := {to_fun := measure_theory.condexp_ind_L1 hm μ s _inst_21, map_add' := _, map_smul' := _}, cont := _}
Conditional expectation of a function as a linear map from α →₁[μ] F'
to itself.
Equations
Auxiliary lemma used in the proof of set_integral_condexp_L1_clm
.
The integral of the conditional expectation condexp_L1_clm
over an m
-measurable set is equal
to the integral of f
on that set. See also set_integral_condexp
, the similar statement for
condexp
.
Conditional expectation of a function, in L1. Its value is 0 if the function is not
integrable. The function-valued condexp
should be used instead in most cases.
Equations
- measure_theory.condexp_L1 hm μ f = measure_theory.set_to_fun μ (measure_theory.condexp_ind hm μ) _ f
The integral of the conditional expectation condexp_L1
over an m
-measurable set is equal to
the integral of f
on that set. See also set_integral_condexp
, the similar statement for
condexp
.
Conditional expectation of a function #
Conditional expectation of a function. It is defined as 0 if any one of the following conditions is true:
m
is not a sub-σ-algebra ofm0
,μ
is not σ-finite with respect tom
,f
is not integrable.
Equations
- measure_theory.condexp m μ f = dite (m ≤ m0) (λ (hm : m ≤ m0), dite (measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ) (λ (h : measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ), ite (measure_theory.strongly_measurable f) f (measure_theory.ae_strongly_measurable'.mk ⇑(measure_theory.condexp_L1 hm μ f) _)) (λ (h : ¬(measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ)), 0)) (λ (hm : ¬m ≤ m0), 0)
The integral of the conditional expectation μ[f|hm]
over an m
-measurable set is equal to
the integral of f
on that set.
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]
.
Lebesgue dominated convergence theorem: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
condexp_L1
.
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.