Theorems · Theorem · measure theory

MeasureTheory.tendsto_condExp_unique

∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (fs gs : ℕ → α → E) (f g : α → E),
  (∀ (n : ℕ), MeasureTheory.Integrable (fs n) μ) →
    (∀ (n : ℕ), MeasureTheory.Integrable (gs n) μ) →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => gs n x) Filter.atTop (nhds (g x))) →
          ∀ (bound_fs : α → ℝ),
            MeasureTheory.Integrable bound_fs μ →
              ∀ (bound_gs : α → ℝ),
                MeasureTheory.Integrable bound_gs μ →
                  (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x) →
                    (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x) →
                      (∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]) → μ[f | m] =ᵐ[μ] μ[g | 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.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

1 results in Mathlib

Foundations

Depth 297 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace