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 of L². This is the orthogonal projection on the subspace of almost everywhere m-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 sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condexpL1CLM : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file MeasureTheory/Integral/SetToL1).
• Define the conditional expectation of a function f : α → E, which is an integrable function α → E equal to 0 if f is not integrable, and equal to an m-measurable representative of condexpL1CLM applied to [f], the equivalence class of f in L¹.

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 of f with respect to m.
• integrable_condexp : condexp is integrable.
• stronglyMeasurable_condexp : condexp is m-strongly-measurable.
• set_integral_condexp (hf : Integrable f μ) (hs : MeasurableSet[m] s) : if m ≤ 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 any m-measurable set s.

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_set_integral_eq: an a.e. m-measurable function which verifies the equality of integrals is a.e. equal to condexp.

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.

Tags

conditional expectation, conditional expected value

theorem MeasureTheory.condexp_def {α : Type u_5} {F' : Type u_6} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] (m : MeasurableSpace α) {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → F') : MeasureTheory.condexp m μ f = if hm : m ≤ m0 then if h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm) ∧ MeasureTheory.Integrable f then if MeasureTheory.StronglyMeasurable f then f else MeasureTheory.AEStronglyMeasurable'.mk ↑↑(MeasureTheory.condexpL1 hm μ f) (_ : MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpL1 hm μ f)) μ) else 0 else 0

@[irreducible]

noncomputable def MeasureTheory.condexp {α : Type u_5} {F' : Type u_6} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] (m : MeasurableSpace α) {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → F') : α → F'

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 of m0,
• μ is not σ-finite with respect to m,
• f is not integrable.

Equations

• @MeasureTheory.condexp = MeasureTheory.wrapped✝.1

def MeasureTheory.«term_[_|_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.condexp_of_not_le {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm_not : ¬m ≤ m0) : MeasureTheory.condexp m μ f = 0

theorem MeasureTheory.condexp_of_not_sigmaFinite {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0) (hμm_not : ¬MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)) : MeasureTheory.condexp m μ f = 0

theorem MeasureTheory.condexp_of_sigmaFinite {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0) [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] : MeasureTheory.condexp m μ f = if MeasureTheory.Integrable f then if MeasureTheory.StronglyMeasurable f then f else MeasureTheory.AEStronglyMeasurable'.mk ↑↑(MeasureTheory.condexpL1 hm μ f) (_ : MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpL1 hm μ f)) μ) else 0

theorem MeasureTheory.condexp_of_stronglyMeasurable {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {f : α → F'} (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f) : MeasureTheory.condexp m μ f = f

theorem MeasureTheory.condexp_const {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (c : F') [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.condexp m μ fun (x : α) => c) = fun (x : α) => c

theorem MeasureTheory.condexp_ae_eq_condexpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (f : α → F') : MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] ↑↑(MeasureTheory.condexpL1 hm μ f)

theorem MeasureTheory.condexp_ae_eq_condexpL1CLM {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hf : MeasureTheory.Integrable f) : MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] ↑↑((MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.Integrable.toL1 f hf))

theorem MeasureTheory.condexp_undef {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hf : ¬MeasureTheory.Integrable f) : MeasureTheory.condexp m μ f = 0

@[simp]

theorem MeasureTheory.condexp_zero {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.condexp m μ 0 = 0

theorem MeasureTheory.stronglyMeasurable_condexp {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} : MeasureTheory.StronglyMeasurable (MeasureTheory.condexp m μ f)

theorem MeasureTheory.condexp_congr_ae {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} {g : α → F'} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ g

theorem MeasureTheory.condexp_of_aestronglyMeasurable' {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {f : α → F'} (hf : MeasureTheory.AEStronglyMeasurable' m f μ) (hfi : MeasureTheory.Integrable f) : MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] f

theorem MeasureTheory.integrable_condexp {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} : MeasureTheory.Integrable (MeasureTheory.condexp m μ f)

theorem MeasureTheory.set_integral_condexp {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} {s : Set α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hf : MeasureTheory.Integrable f) (hs : MeasurableSet s) : ∫ (x : α) in s, MeasureTheory.condexp m μ f x ∂μ = ∫ (x : α) in s, f x ∂μ

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} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0) [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hf : MeasureTheory.Integrable f) : ∫ (x : α), MeasureTheory.condexp m μ f x ∂μ = ∫ (x : α), f x ∂μ

theorem MeasureTheory.ae_eq_condexp_of_forall_set_integral_eq {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {f : α → F'} {g : α → F'} (hf : MeasureTheory.Integrable f) (hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn g s) (hg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ) (hgm : MeasureTheory.AEStronglyMeasurable' m g μ) : g =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ f

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} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hμ : NeZero μ] (f : α → F') : MeasureTheory.condexp ⊥ μ f = fun (x : α) => (ENNReal.toReal (↑↑μ Set.univ))⁻¹ • ∫ (x : α), f x ∂μ

theorem MeasureTheory.condexp_bot_ae_eq {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → F') : MeasureTheory.condexp ⊥ μ f =ᶠ[MeasureTheory.Measure.ae μ] fun (x : α) => (ENNReal.toReal (↑↑μ Set.univ))⁻¹ • ∫ (x : α), f x ∂μ

theorem MeasureTheory.condexp_bot {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (f : α → F') : MeasureTheory.condexp ⊥ μ f = fun (x : α) => ∫ (x : α), f x ∂μ

theorem MeasureTheory.condexp_add {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} {g : α → F'} (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : MeasureTheory.condexp m μ (f + g) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ f + MeasureTheory.condexp m μ g

theorem MeasureTheory.condexp_finset_sum {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {s : Finset ι} {f : ι → α → F'} (hf : ∀ i ∈ s, MeasureTheory.Integrable (f i)) : MeasureTheory.condexp m μ (Finset.sum s fun (i : ι) => f i) =ᶠ[MeasureTheory.Measure.ae μ] Finset.sum s fun (i : ι) => MeasureTheory.condexp m μ (f i)

theorem MeasureTheory.condexp_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : 𝕜) (f : α → F') : MeasureTheory.condexp m μ (c • f) =ᶠ[MeasureTheory.Measure.ae μ] c • MeasureTheory.condexp m μ f

theorem MeasureTheory.condexp_neg {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → F') : MeasureTheory.condexp m μ (-f) =ᶠ[MeasureTheory.Measure.ae μ] -MeasureTheory.condexp m μ f

theorem MeasureTheory.condexp_sub {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} {g : α → F'} (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : MeasureTheory.condexp m μ (f - g) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ f - MeasureTheory.condexp m μ g

theorem MeasureTheory.condexp_condexp_of_le {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {f : α → F'} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm₁₂ : m₁ ≤ m₂) (hm₂ : m₂ ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm₂)] : MeasureTheory.condexp m₁ μ (MeasureTheory.condexp m₂ μ f) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m₁ μ f

theorem MeasureTheory.condexp_mono {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] [OrderedSMul ℝ E] {f : α → E} {g : α → E} (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) (hfg : f ≤ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.condexp m μ f ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ g

theorem MeasureTheory.condexp_nonneg {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] [OrderedSMul ℝ E] {f : α → E} (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] f) : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ f

theorem MeasureTheory.condexp_nonpos {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] [OrderedSMul ℝ E] {f : α → E} (hf : f ≤ᶠ[MeasureTheory.Measure.ae μ] 0) : MeasureTheory.condexp m μ f ≤ᶠ[MeasureTheory.Measure.ae μ] 0

theorem MeasureTheory.tendsto_condexpL1_of_dominated_convergence {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {fs : ℕ → α → F'} {f : α → F'} (bound_fs : α → ℝ) (hfs_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ) (h_int_bound_fs : MeasureTheory.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 : ℕ) => MeasureTheory.condexpL1 hm μ (fs n)) Filter.atTop (nhds (MeasureTheory.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} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (fs : ℕ → α → F') (gs : ℕ → α → F') (f : α → F') (g : α → F') (hfs_int : ∀ (n : ℕ), MeasureTheory.Integrable (fs n)) (hgs_int : ∀ (n : ℕ), MeasureTheory.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 : MeasureTheory.Integrable bound_fs) (bound_gs : α → ℝ) (h_int_bound_gs : MeasureTheory.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 : ℕ), MeasureTheory.condexp m μ (fs n) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ (gs n)) : MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ g

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.