Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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 .

The construction is done in four steps:

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

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

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

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 (μ.trim hm) MeasureTheory.Integrable f μ then if MeasureTheory.StronglyMeasurable f then f else MeasureTheory.AEStronglyMeasurable'.mk (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
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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) :
      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 (μ.trim hm)) :
      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 (μ.trim hm)] (f : αF') :
      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 μ) :
      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 =ᵐ[μ] g) :
      theorem MeasureTheory.setIntegral_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 (μ.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.

      @[deprecated MeasureTheory.setIntegral_condexp]
      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 (μ.trim hm)] (hf : MeasureTheory.Integrable f μ) (hs : MeasurableSet s) :
      ∫ (x : α) in s, MeasureTheory.condexp m μ f xμ = ∫ (x : α) in s, f xμ

      Alias of MeasureTheory.setIntegral_condexp.


      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 (μ.trim hm)] :
      ∫ (x : α), MeasureTheory.condexp m μ f xμ = ∫ (x : α), f xμ
      theorem MeasureTheory.integral_condexp_indicator {α : Type u_1} {F : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [mF : MeasurableSpace F] {Y : αF} (hY : Measurable Y) [MeasureTheory.SigmaFinite (μ.trim )] {A : Set α} (hA : MeasurableSet A) :
      ∫ (x : α), MeasureTheory.condexp (MeasurableSpace.comap Y mF) μ (A.indicator fun (x : α) => 1) xμ = (μ A).toReal

      Total probability law using condexp as conditional probability.

      theorem MeasureTheory.ae_eq_condexp_of_forall_setIntegral_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 (μ.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 μ) :

      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].

      @[deprecated MeasureTheory.ae_eq_condexp_of_forall_setIntegral_eq]
      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 (μ.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 μ) :

      Alias of MeasureTheory.ae_eq_condexp_of_forall_setIntegral_eq.


      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 : α) => (μ Set.univ).toReal⁻¹ ∫ (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 =ᵐ[μ] fun (x : α) => (μ Set.univ).toReal⁻¹ ∫ (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 μ) :
      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 : is, MeasureTheory.Integrable (f i) μ) :
      MeasureTheory.condexp m μ (is, f i) =ᵐ[μ] is, MeasureTheory.condexp m μ (f i)
      theorem MeasureTheory.condexp_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : 𝕜) (f : α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 μ) :
      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 (μ.trim hm₂)] :
      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 ≤ᵐ[μ] g) :
      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 (μ.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.condexp m μ (gs n)) :

      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.