Theorems · Theorem · probability

ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} [inst : LinearOrder ι] {i j : ι}
  {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)),
  ProbabilityTheory.iIndepSet s μ →
    i < j → μ[(s j).indicator fun x => 1 | ↑(MeasureTheory.filtrationOfSet hsm) i] =ᵐ[μ] fun x => μ.real (s j)

Defined in

Mathlib.Probability.BorelCantelli

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrder