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 ∈ Eto 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α → Eequal to 0 iffis not integrable, and equal to anm-measurable representative ofcondExpL1CLMapplied to[f], the equivalence class offinL¹.
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 offwith respect tom.integrable_condExp:condExpis integrable.stronglyMeasurable_condExp:condExpism-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.
Notation #
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
@[irreducible]
noncomputable def
MeasureTheory.condExp
{α : Type u_5}
{E : Type u_6}
(m : MeasurableSpace α)
{m₀ : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(μ : Measure α)
(f : α → E)
:
α → E
Conditional expectation of a function, with notation μ[f|m].
It is defined as 0 if any one of the following conditions is true:
mis not a sub-σ-algebra ofm₀,μis not σ-finite with respect tom,fis not integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.condExp_def
{α : Type u_5}
{E : Type u_6}
(m : MeasurableSpace α)
{m₀ : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(μ : Measure α)
(f : α → E)
:
μ[f|m] = if hm : m ≤ m₀ then
if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
if StronglyMeasurable f then f
else have this := ⋯;
AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
else 0
else 0
Conditional expectation of a function, with notation μ[f|m].
It is defined as 0 if any one of the following conditions is true:
mis not a sub-σ-algebra ofm₀,μis not σ-finite with respect tom,fis 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
theorem
MeasureTheory.condExp_of_not_le
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm_not : ¬m ≤ m₀)
:
theorem
MeasureTheory.condExp_of_not_sigmaFinite
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
(hμm_not : ¬SigmaFinite (μ.trim hm))
:
theorem
MeasureTheory.condExp_of_sigmaFinite
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
:
μ[f|m] = if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0
theorem
MeasureTheory.condExp_of_stronglyMeasurable
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
{f : α → E}
(hf : StronglyMeasurable f)
(hfi : Integrable f μ)
:
@[simp]
theorem
MeasureTheory.condExp_const
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
(c : E)
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.condExp_ae_eq_condExpL1
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
(f : α → E)
:
theorem
MeasureTheory.condExp_ae_eq_condExpL1CLM
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
(hf : Integrable f μ)
:
theorem
MeasureTheory.condExp_of_not_integrable
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hf : ¬Integrable f μ)
:
@[simp]
theorem
MeasureTheory.condExp_zero
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
theorem
MeasureTheory.stronglyMeasurable_condExp
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
theorem
MeasureTheory.condExp_congr_ae
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(h : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.condExp_congr_ae_trim
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.condExp_of_aestronglyMeasurable'
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.integrable_condExp
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
Integrable μ[f|m] μ
theorem
MeasureTheory.setIntegral_condExp
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
{s : Set α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
(hf : Integrable f μ)
(hs : MeasurableSet s)
:
The integral of the conditional expectation μ[f|hm] over an m-measurable set is equal to
the integral of f on that set.
theorem
MeasureTheory.integral_condExp
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
:
theorem
MeasureTheory.integral_condExp_indicator
{α : Type u_1}
{β : Type u_2}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[mβ : MeasurableSpace β]
{Y : α → β}
(hY : Measurable Y)
[SigmaFinite (μ.trim ⋯)]
{A : Set α}
(hA : MeasurableSet A)
:
Law of total probability using condExp as conditional probability.
theorem
MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
{f g : α → E}
(hf : Integrable f μ)
(hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ)
(hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ)
(hgm : AEStronglyMeasurable g μ)
:
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].
theorem
MeasureTheory.condExp_bot'
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[hμ : NeZero μ]
(f : α → E)
:
theorem
MeasureTheory.condExp_bot_ae_eq
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : α → E)
:
theorem
MeasureTheory.condExp_bot
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[IsProbabilityMeasure μ]
(f : α → E)
:
theorem
MeasureTheory.condExp_add
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hf : Integrable f μ)
(hg : Integrable g μ)
(m : MeasurableSpace α)
:
theorem
MeasureTheory.condExp_finset_sum
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_5}
{s : Finset ι}
{f : ι → α → E}
(hf : ∀ i ∈ s, Integrable (f i) μ)
(m : MeasurableSpace α)
:
theorem
MeasureTheory.condExp_smul
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_4}
[RCLike 𝕜]
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedSpace 𝕜 E]
(c : 𝕜)
(f : α → E)
(m : MeasurableSpace α)
:
theorem
MeasureTheory.condExp_neg
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : α → E)
(m : MeasurableSpace α)
:
theorem
MeasureTheory.condExp_sub
{α : Type u_1}
{E : Type u_3}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hf : Integrable f μ)
(hg : Integrable g μ)
(m : MeasurableSpace α)
:
theorem
MeasureTheory.condExp_condExp_of_le
{α : Type u_1}
{E : Type u_3}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{m₁ m₂ m₀ : MeasurableSpace α}
{μ : Measure α}
(hm₁₂ : m₁ ≤ m₂)
(hm₂ : m₂ ≤ m₀)
[SigmaFinite (μ.trim 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.
theorem
MeasureTheory.MemLp.condExpL2_ae_eq_condExp'
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_4}
[RCLike 𝕜]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[InnerProductSpace 𝕜 E]
(hm : m ≤ m₀)
(hf1 : Integrable f μ)
(hf2 : MemLp f 2 μ)
[SigmaFinite (μ.trim hm)]
:
theorem
MeasureTheory.MemLp.condExpL2_ae_eq_condExp
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_4}
[RCLike 𝕜]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[InnerProductSpace 𝕜 E]
(hm : m ≤ m₀)
(hf : MemLp f 2 μ)
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.eLpNorm_condExp_le
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[InnerProductSpace ℝ E]
:
theorem
MeasureTheory.MemLp.condExp
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[InnerProductSpace ℝ E]
(hf : MemLp f 2 μ)
:
@[simp]
theorem
MeasureTheory.condExp_ofNat
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{R : Type u_5}
[NormedRing R]
[NormedSpace ℝ R]
[CompleteSpace R]
(n : ℕ)
[n.AtLeastTwo]
(f : α → R)
:
theorem
MeasureTheory.tendsto_condExpL1_of_dominated_convergence
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
{fs : ℕ → α → E}
{f : α → E}
(bound_fs : α → ℝ)
(hfs_meas : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ)
(h_int_bound_fs : Integrable bound_fs μ)
(hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x)
(hfs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n x) Filter.atTop (nhds (f x)))
:
Filter.Tendsto (fun (n : ℕ) => condExpL1 hm μ (fs n)) Filter.atTop (nhds (condExpL1 hm μ f))
Lebesgue dominated convergence theorem: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
condExpL1.
theorem
MeasureTheory.tendsto_condExp_unique
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
(fs gs : ℕ → α → E)
(f g : α → E)
(hfs_int : ∀ (n : ℕ), Integrable (fs n) μ)
(hgs_int : ∀ (n : ℕ), Integrable (gs n) μ)
(hfs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n x) Filter.atTop (nhds (f x)))
(hgs : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => gs n x) Filter.atTop (nhds (g x)))
(bound_fs : α → ℝ)
(h_int_bound_fs : Integrable bound_fs μ)
(bound_gs : α → ℝ)
(h_int_bound_gs : Integrable bound_gs μ)
(hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x)
(hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x)
(hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m])
:
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.
theorem
MeasureTheory.condExp_mono
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[NormedAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
(hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : f ≤ᶠ[ae μ] g)
:
theorem
MeasureTheory.condExp_nonneg
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
(hf : 0 ≤ᶠ[ae μ] f)
:
theorem
MeasureTheory.condExp_nonpos
{α : Type u_1}
{E : Type u_3}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
[NormedAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
(hf : f ≤ᶠ[ae μ] 0)
: