Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {β : Type u_3}
  [inst : LinearOrder ι] [mβ : MeasurableSpace β] [inst_1 : NormedAddCommGroup β] [inst_2 : BorelSpace β]
  {f : ι → Ω → β} {i j : ι} [SecondCountableTopology β] [CompleteSpace β] [inst_5 : NormedSpace ℝ β]
  (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)),
  ProbabilityTheory.iIndepFun f μ →
    i < j → μ[f j | ↑(MeasureTheory.Filtration.natural f hf) i] =ᵐ[μ] fun x => ∫ (x : Ω), f j x ∂μ

Defined in

Mathlib.Probability.BorelCantelli

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderMeasurableSpaceNormedAddCommGroupBorelSpaceSecondCountableTopologyCompleteSpaceNormedSpace