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 ∈ 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 ≤ 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 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 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 (μ.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:
mis not a sub-σ-algebra ofm0,μis not σ-finite with respect tom,fis 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)
:
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 (μ.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 (μ.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) ⋯
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 (μ.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 (μ.trim hm)]
(f : α → F')
:
MeasureTheory.condexp m μ f =ᵐ[μ] ↑↑(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 (μ.trim hm)]
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexp m μ f =ᵐ[μ] ↑↑((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'}
:
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)
:
MeasureTheory.condexp m μ f =ᵐ[μ] 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 (μ.trim hm)]
{f : α → F'}
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hfi : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexp m μ f =ᵐ[μ] 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'}
:
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 μ)
:
g =ᵐ[μ] 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].
@[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 μ)
:
g =ᵐ[μ] MeasureTheory.condexp m μ f
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')
:
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.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 μ (∑ i ∈ s, f i) =ᵐ[μ] ∑ i ∈ s, 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')
:
MeasureTheory.condexp m μ (c • f) =ᵐ[μ] 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.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.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 (μ.trim hm₂)]
:
MeasureTheory.condexp m₁ μ (MeasureTheory.condexp m₂ μ f) =ᵐ[μ] 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 ≤ᵐ[μ] g)
:
MeasureTheory.condexp m μ f ≤ᵐ[μ] 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 ≤ᵐ[μ] f)
:
0 ≤ᵐ[μ] 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 ≤ᵐ[μ] 0)
:
MeasureTheory.condexp m μ f ≤ᵐ[μ] 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 (μ.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))
:
MeasureTheory.condexp m μ f =ᵐ[μ] 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.